let H be ZF-formula; :: thesis: for x being Variable
for E being non empty set holds
( E |= All (x,H) iff E |= H )
let x be Variable; :: thesis: for E being non empty set holds
( E |= All (x,H) iff E |= H )
let E be non empty set ; :: thesis: ( E |= All (x,H) iff E |= H )
thus ( E |= All (x,H) implies E |= H ) :: thesis: ( E |= H implies E |= All (x,H) )

proof

assume A1: for f being Function of VAR,E holds E,f |= All (x,H) ; :: according to ZF_MODEL:def 5 :: thesis: E |= H
let f be Function of VAR,E; :: according to ZF_MODEL:def 5 :: thesis: E,f |= H
for y being Variable st f . y <> f . y holds
x = y ;
hence E,f |= H by A1, Th16; :: thesis: verum

end;

assume A2: E |= H ; :: thesis: E |= All (x,H)
let f be Function of VAR,E; :: according to ZF_MODEL:def 5 :: thesis: E,f |= All (x,H)
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 A2;
hence E,f |= All (x,H) by Th16; :: thesis: verum