let E be non empty set ; for f being Function of VAR,E
for H being ZF-formula
for x being Variable holds
( E,f |= Ex (x,H) iff ex g being Function of VAR,E st
( ( for y being Variable st g . y <> f . y holds
x = y ) & E,g |= H ) )
let f be Function of VAR,E; for H being ZF-formula
for x being Variable holds
( E,f |= Ex (x,H) iff ex g being Function of VAR,E st
( ( for y being Variable st g . y <> f . y holds
x = y ) & E,g |= H ) )
let H be ZF-formula; for x being Variable holds
( E,f |= Ex (x,H) iff ex g being Function of VAR,E st
( ( for y being Variable st g . y <> f . y holds
x = y ) & E,g |= H ) )
let x be Variable; ( E,f |= Ex (x,H) iff ex g being Function of VAR,E st
( ( for y being Variable st g . y <> f . y holds
x = y ) & E,g |= H ) )
thus
( E,f |= Ex (x,H) implies ex g being Function of VAR,E st
( ( for y being Variable st g . y <> f . y holds
x = y ) & E,g |= H ) )
( ex g being Function of VAR,E st
( ( for y being Variable st g . y <> f . y holds
x = y ) & E,g |= H ) implies E,f |= Ex (x,H) )proof
assume
E,
f |= Ex (
x,
H)
;
ex g being Function of VAR,E st
( ( for y being Variable st g . y <> f . y holds
x = y ) & E,g |= H )
then consider g being
Function of
VAR,
E such that A1:
for
y being
Variable st
g . y <> f . y holds
x = y
and A2:
not
E,
g |= 'not' H
by Th14, Th16;
thus
ex
g being
Function of
VAR,
E st
( ( for
y being
Variable st
g . y <> f . y holds
x = y ) &
E,
g |= H )
by A1, A2, Th14;
verum
end;
given g being Function of VAR,E such that A3:
for y being Variable st g . y <> f . y holds
x = y
and
A4:
E,g |= H
; E,f |= Ex (x,H)
not E,g |= 'not' H
by A4, Th14;
hence
E,f |= Ex (x,H)
by Th14, A3, Th16; verum