theorem Th9: :: ZFMODEL2:9

for x being Variable
for M being non empty set
for m being Element of M
for H being ZF-formula
for v being Function of VAR,M st not x in Free H holds
( M,v |= H iff M,v / (x,m) |= H )