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

A2: for y being Variable st f . y <> f . y holds
x = y ;
assume 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
hence E,f |= H by A2; :: thesis: verum

end;

A3: ( ( 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) ) by Def4;
thus ( 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 A3, A1, Th6; :: thesis: verum