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

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:130;
then g . z = f . z by A8, A11;
hence contradiction by A10, A12, FUNCT_7:34; :: 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:34;
hence E,f |= Ex x,y,H by A13, Th20; :: thesis: verum