let H be ZF-formula; for x being Variable
for E being non empty set holds
( E |= All (x,H) iff E |= H )
let x be Variable; for E being non empty set holds
( E |= All (x,H) iff E |= H )
let E be non empty set ; ( E |= All (x,H) iff E |= H )
thus
( E |= All (x,H) implies E |= H )
( E |= H implies E |= All (x,H) )
assume A2:
E |= H
; E |= All (x,H)
let f be Function of VAR,E; ZF_MODEL:def 5 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; verum