theorem Th12: :: ZFMODEL2:12

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