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 ) )
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
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; :: thesis: 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 ; :: thesis: E,f |= Ex (x,H)
not E,g |= 'not' H by A4, Th14;
hence E,f |= Ex (x,H) by Th14, A3, Th16; :: thesis: verum