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
A2: 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;

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 A3: for z being Variable holds
( not g . z <> f . z or x = z or y = z ) ; :: thesis: E,g |= H
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
A4: (g +* (y,(f . y))) . z <> f . z and
A5: x <> z ; :: thesis: contradiction
A6: y <> z by A4, FUNCT_7:128;
then g . z = f . z by A3, A5;
hence contradiction by A4, A6, FUNCT_7:32; :: thesis: verum

end;

then ( ( for z being Variable st g . z <> (g +* (y,(f . y))) . z holds
y = z ) implies E,g |= H ) by A2;
hence E,g |= H by FUNCT_7:32; :: 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 :: thesis: for g being Function of VAR,E st ( for z being Variable st g . z <> f . z holds
x = z ) holds
E,g |= All (y,H)

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 :: 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

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 :: thesis: for z being Variable st h . z <> f . z & x <> z holds
not y <> z

let z be Variable; :: thesis: ( h . z <> f . z & x <> z implies not y <> z )
assume that
A10: ( h . z <> f . z & x <> z ) and
A11: y <> z ; :: thesis: contradiction
h . z = g . z by A9, A11;
hence contradiction by A8, A10; :: 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