theorem :: ZFMODEL2:15

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