theorem Th2: :: ZFMODEL2:2

for x, y being Variable
for H being ZF-formula st not y in variables_in H holds
( ( x in Free H implies Free (H / (x,y)) = ((Free H) \ {x}) \/ {y} ) & ( not x in Free H implies Free (H / (x,y)) = Free H ) )