let E be non empty set ; :: thesis: for f being Function of VAR ,E
for H being ZF-formula
for x being Variable holds
( E,f |= All x,H iff for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
E,g |= H )
let f be Function of VAR ,E; :: thesis: for H being ZF-formula
for x being Variable holds
( E,f |= All x,H iff for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
E,g |= H )
let H be ZF-formula; :: thesis: for x being Variable holds
( E,f |= All x,H iff for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
E,g |= H )
let x be Variable; :: thesis: ( E,f |= All x,H iff for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
E,g |= H )
A1: ( ( E,f |= H implies f in St H,E ) & ( f in St H,E implies E,f |= H ) & ( E,f |= All x,H implies f in St (All x,H),E ) & ( f in St (All x,H),E implies E,f |= All x,H ) & ( f in St (All x,H),E implies ( f in St H,E & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St H,E ) ) ) & ( f in St H,E & ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St H,E ) implies f in St (All x,H),E ) ) by Def4, Th6;
A2: ( ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St H,E ) implies for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
E,g |= H )

proof

assume A3: for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St H,E ; :: thesis: for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
E,g |= H
let g be Function of VAR ,E; :: thesis: ( ( for y being Variable st g . y <> f . y holds
x = y ) implies E,g |= H )
assume for y being Variable st g . y <> f . y holds
x = y ; :: thesis: E,g |= H
then g in St H,E by A3;
hence E,g |= H by Def4; :: thesis: verum

end;

A4: ( ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
E,g |= H ) implies for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St H,E )

proof

assume A5: for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
E,g |= H ; :: thesis: for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in St H,E
let g be Function of VAR ,E; :: thesis: ( ( for y being Variable st g . y <> f . y holds
x = y ) implies g in St H,E )
assume for y being Variable st g . y <> f . y holds
x = y ; :: thesis: g in St H,E
then E,g |= H by A5;
hence g in St H,E by Def4; :: thesis: verum

end;

( ( for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
E,g |= H ) implies E,f |= H )

proof

assume A6: for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
E,g |= H ; :: thesis: E,f |= H
for y being Variable st f . y <> f . y holds
x = y ;
hence E,f |= H by A6; :: thesis: verum

end;

hence ( E,f |= All x,H iff for g being Function of VAR ,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
E,g |= H ) by A1, A2, A4; :: thesis: verum