theorem Th10: :: ZFMODEL1:10

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