theorem Th11: :: ZFMODEL1:11

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