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 |= All x,y,H iff for g being Function of VAR ,E st ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) holds
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 |= All x,y,H iff for g being Function of VAR ,E st ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) holds
E,g |= H )
let E be non empty set ; :: thesis: for f being Function of VAR ,E holds
( E,f |= All x,y,H iff for g being Function of VAR ,E st ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) holds
E,g |= H )
let f be Function of VAR ,E; :: thesis: ( E,f |= All x,y,H iff for g being Function of VAR ,E st ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) holds
E,g |= H )
thus ( E,f |= All x,y,H implies for g being Function of VAR ,E st ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) holds
E,g |= H ) :: thesis: ( ( for g being Function of VAR ,E st ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) holds
E,g |= H ) implies E,f |= All x,y,H )

proof

assume A1: E,f |= All x,y,H ; :: thesis: for g being Function of VAR ,E st ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) holds
E,g |= H
let g be Function of VAR ,E; :: thesis: ( ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) implies E,g |= H )
assume A2: for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ; :: thesis: E,g |= H
A3: for g being Function of VAR ,E st ( for z being Variable st g . z <> f . z holds
x = z ) holds
for h being Function of VAR ,E st ( for z being Variable st h . z <> g . z holds
y = z ) holds
E,h |= H

proof

let g be Function of VAR ,E; :: thesis: ( ( for z being Variable st g . z <> f . z holds
x = z ) implies for h being Function of VAR ,E st ( for z being Variable st h . z <> g . z holds
y = z ) holds
E,h |= H )
assume for z being Variable st g . z <> f . z holds
x = z ; :: thesis: for h being Function of VAR ,E st ( for z being Variable st h . z <> g . z holds
y = z ) holds
E,h |= H
then E,g |= All y,H by A1, Th16;
hence for h being Function of VAR ,E st ( for z being Variable st h . z <> g . z holds
y = z ) holds
E,h |= H by Th16; :: thesis: verum

end;

set h = g +* y,(f . y);
for z being Variable st (g +* y,(f . y)) . z <> f . z holds
x = z

proof

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

end;

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

end;

assume A7: for g being Function of VAR ,E st ( for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ) holds
E,g |= H ; :: thesis: E,f |= All x,y,H

now

let g be Function of VAR ,E; :: thesis: ( ( for z being Variable st g . z <> f . z holds
x = z ) implies E,g |= All y,H )
assume A8: for z being Variable st g . z <> f . z holds
x = z ; :: thesis: E,g |= All y,H

now

let h be Function of VAR ,E; :: thesis: ( ( for z being Variable st h . z <> g . z holds
y = z ) implies E,h |= H )
assume A9: for z being Variable st h . z <> g . z holds
y = z ; :: thesis: E,h |= H

now

let z be Variable; :: thesis: ( h . z <> f . z & x <> z implies not y <> z )
assume ( h . z <> f . z & x <> z & y <> z ) ; :: thesis: contradiction
then ( h . z <> f . z & h . z = g . z & g . z = f . z ) by A8, A9;
hence contradiction ; :: thesis: verum

end;

hence E,h |= H by A7; :: thesis: verum

end;

hence E,g |= All y,H by Th16; :: thesis: verum

end;

hence E,f |= All x,y,H by Th16; :: thesis: verum