let H be ZF-formula; :: thesis:
let x, y be Variable; :: thesis:
let E be non empty set ; :: thesis:
let f be Function of VAR,E; :: thesis:
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:

proof

assume E,f |= Ex (x,y,H) ; :: thesis:
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:
thus for z being Variable holds
( not h . z <> f . z or x = z or y = z ) :: thesis:

proof

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

end;

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

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:
set h = f +* (x,(g . x));

now :: thesis:

let z be Variable; :: thesis:
assume that
A10: g . z <> (f +* (x,(g . x))) . z and
A11: y <> z ; :: thesis:
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:

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: