let E be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) )
A1: ( E,f |= 'not' (All (x,('not' H))) iff not E,f |= All (x,('not' H)) ) by Th14;
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 ) ) :: thesis: ( 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) ; :: thesis: 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
A2: for y being Variable st g . y <> f . y holds
x = y and
A3: not E,g |= 'not' H by A1, Th16;
E,g |= H by A3, Th14;
hence ex g being Function of VAR,E st
( ( for y being Variable st g . y <> f . y holds
x = y ) & E,g |= H ) by A2; :: thesis: verum

end;

given g being Function of VAR,E such that A4: for y being Variable st g . y <> f . y holds
x = y and
A5: E,g |= H ; :: thesis: E,f |= Ex (x,H)
not E,g |= 'not' H by A5, Th14;
hence E,f |= Ex (x,H) by A1, A4, Th16; :: thesis: verum