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 ) & E,g |= Ex y,H ) by Th20;
consider h being Function of VAR ,E such that
A2: ( ( for z being Variable st h . z <> g . z holds
y = z ) & E,h |= H ) by A1, 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
A3: h . z <> f . z and
A4: ( x <> z & y <> z ) ; :: thesis: contradiction
( g . z = f . z & h . z = g . z ) by A1, A2, A4;
hence contradiction by A3; :: thesis: verum

end;

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

end;

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

now

let z be Variable; :: thesis: ( g . z <> (f +* x,(g . x)) . z implies not y <> z )
assume A7: ( g . z <> (f +* x,(g . x)) . z & y <> z ) ; :: thesis: contradiction
then x <> z by FUNCT_7:130;
then ( g . z = f . z & (f +* x,(g . x)) . z = f . z ) by A5, FUNCT_7:34, A7;
hence contradiction by A7; :: thesis: verum

end;

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