theorem :: ZFMODEL1:12

for x, y, z being Variable
for H being ZF-formula
for E being non empty set
for f being Function of VAR,E st {x,y,z} misses Free H & E,f |= H holds
E,f |= All (x,y,z,H)