let H be ZF-formula; :: thesis: for x, y being Variable
for E being non empty set
for f being Function of VAR,E holds
( E,f |= Ex (x,y,H) iff ex g being Function of VAR,E st
( ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) )
let x, y be Variable; :: thesis: for E being non empty set
for f being Function of VAR,E holds
( E,f |= Ex (x,y,H) iff ex g being Function of VAR,E st
( ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) )
let E be non empty set ; :: thesis: for f being Function of VAR,E holds
( E,f |= Ex (x,y,H) iff ex g being Function of VAR,E st
( ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) )
let f be Function of VAR,E; :: thesis: ( E,f |= Ex (x,y,H) iff ex g being Function of VAR,E st
( ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) )
thus ( E,f |= Ex (x,y,H) implies ex g being Function of VAR,E st
( ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) ) :: thesis: ( ex g being Function of VAR,E st
( ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) implies E,f |= Ex (x,y,H) )

proof

assume E,f |= Ex (x,y,H) ; :: thesis: ex g being Function of VAR,E st
( ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) & E,g |= H )
then consider g being Function of VAR,E such that
A1: for z being Variable st g . z <> f . z holds
x = z and
A2: E,g |= Ex (y,H) by Th20;
consider h being Function of VAR,E such that
A3: for z being Variable st h . z <> g . z holds
y = z and
A4: E,h |= H by A2, Th20;
take h ; :: thesis: ( ( for z being Variable holds
( not h . z <> f . z or x = z or y = z ) ) & E,h |= H )
thus for z being Variable holds
( not h . z <> f . z or x = z or y = z ) :: thesis: E,h |= H

proof

let z be Variable; :: thesis: ( not h . z <> f . z or x = z or y = z )
assume that
A5: h . z <> f . z and
A6: x <> z and
A7: y <> z ; :: thesis: contradiction
g . z = f . z by A1, A6;
hence contradiction by A3, A5, A7; :: thesis: verum

end;

thus E,h |= H by A4; :: thesis: verum

end;

given g being Function of VAR,E such that A8: for z being Variable holds
( not g . z <> f . z or x = z or y = z ) and
A9: E,g |= H ; :: thesis: E,f |= Ex (x,y,H)
set h = f +* (x,(g . x));

now :: thesis: for z being Variable st g . z <> (f +* (x,(g . x))) . z holds
not y <> z

let z be Variable; :: thesis: ( g . z <> (f +* (x,(g . x))) . z implies not y <> z )
assume that
A10: g . z <> (f +* (x,(g . x))) . z and
A11: y <> z ; :: thesis: contradiction
A12: x <> z by A10, FUNCT_7:128;
then g . z = f . z by A8, A11;
hence contradiction by A10, A12, FUNCT_7:32; :: thesis: verum

end;

then A13: E,f +* (x,(g . x)) |= Ex (y,H) by A9, Th20;
for z being Variable st (f +* (x,(g . x))) . z <> f . z holds
x = z by FUNCT_7:32;
hence E,f |= Ex (x,y,H) by A13, Th20; :: thesis: verum