theorem Th5: :: ZFMODEL2:5

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 variables_in H holds
( M,v |= H iff M,v / (x,m) |= H )