theorem Th13: :: ZFMODEL2:13

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 & M,v |= H holds
M,v / (x,(v . y)) |= H / (y,x)