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

end;

assume A3: 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 A3, Def5;
hence E,f |= All x,H by Th16; :: thesis: verum