let H be ZF-formula; :: thesis: for y, x being Variable st not y in variables_in H & x <> x. 0 & y <> x. 0 & y <> x. 4 holds
( x. 4 in Free H iff x. 0 in Free (Ex (x. 3),(((x. 3) 'in' x) '&' ((H / (x. 0 ),y) / (x. 4),(x. 0 )))) )
let y, x be Variable; :: thesis: ( not y in variables_in H & x <> x. 0 & y <> x. 0 & y <> x. 4 implies ( x. 4 in Free H iff x. 0 in Free (Ex (x. 3),(((x. 3) 'in' x) '&' ((H / (x. 0 ),y) / (x. 4),(x. 0 )))) ) )
A1: x. 0 <> x. 3 by ZF_LANG1:86;
assume that
A2: not y in variables_in H and
A3: x <> x. 0 and
A4: y <> x. 0 and
A5: y <> x. 4 ; :: thesis: ( x. 4 in Free H iff x. 0 in Free (Ex (x. 3),(((x. 3) 'in' x) '&' ((H / (x. 0 ),y) / (x. 4),(x. 0 )))) )
set G = (H / (x. 0 ),y) / (x. 4),(x. 0 );
A6: Free (Ex (x. 3),(((x. 3) 'in' x) '&' ((H / (x. 0 ),y) / (x. 4),(x. 0 )))) = (Free (((x. 3) 'in' x) '&' ((H / (x. 0 ),y) / (x. 4),(x. 0 )))) \ {(x. 3)} by ZF_LANG1:71
.= ((Free ((x. 3) 'in' x)) \/ (Free ((H / (x. 0 ),y) / (x. 4),(x. 0 )))) \ {(x. 3)} by ZF_LANG1:66
.= ({(x. 3),x} \/ (Free ((H / (x. 0 ),y) / (x. 4),(x. 0 )))) \ {(x. 3)} by ZF_LANG1:64
.= ({(x. 3),x} \ {(x. 3)}) \/ ((Free ((H / (x. 0 ),y) / (x. 4),(x. 0 ))) \ {(x. 3)}) by XBOOLE_1:42 ;
A7: x. 0 <> x. 4 by ZF_LANG1:86;

A8: now

assume A9: x. 4 in Free H ; :: thesis: x. 0 in Free (Ex (x. 3),(((x. 3) 'in' x) '&' ((H / (x. 0 ),y) / (x. 4),(x. 0 ))))
A10: x. 4 in Free (H / (x. 0 ),y)

proof

now

per cases ( x. 0 in Free H or not x. 0 in Free H ) ;

suppose A11: x. 0 in Free H ; :: thesis: x. 4 in Free (H / (x. 0 ),y)

not x. 4 in {(x. 0 )} by A7, TARSKI:def 1;
then A12: x. 4 in (Free H) \ {(x. 0 )} by A9, XBOOLE_0:def 5;
Free (H / (x. 0 ),y) = ((Free H) \ {(x. 0 )}) \/ {y} by A2, A11, ZFMODEL2:2;
hence x. 4 in Free (H / (x. 0 ),y) by A12, XBOOLE_0:def 3; :: thesis: verum

end;

suppose not x. 0 in Free H ; :: thesis: x. 4 in Free (H / (x. 0 ),y)

hence x. 4 in Free (H / (x. 0 ),y) by A2, A9, ZFMODEL2:2; :: thesis: verum

end;

end;

end;

hence x. 4 in Free (H / (x. 0 ),y) ; :: thesis: verum

end;

A13: x. 0 in {(x. 0 )} by TARSKI:def 1;
not x. 0 in variables_in (H / (x. 0 ),y) by A4, ZF_LANG1:198;
then Free ((H / (x. 0 ),y) / (x. 4),(x. 0 )) = ((Free (H / (x. 0 ),y)) \ {(x. 4)}) \/ {(x. 0 )} by A10, ZFMODEL2:2;
then A14: x. 0 in Free ((H / (x. 0 ),y) / (x. 4),(x. 0 )) by A13, XBOOLE_0:def 3;
not x. 0 in {(x. 3)} by A1, TARSKI:def 1;
then x. 0 in (Free ((H / (x. 0 ),y) / (x. 4),(x. 0 ))) \ {(x. 3)} by A14, XBOOLE_0:def 5;
hence x. 0 in Free (Ex (x. 3),(((x. 3) 'in' x) '&' ((H / (x. 0 ),y) / (x. 4),(x. 0 )))) by A6, XBOOLE_0:def 3; :: thesis: verum

end;

now

assume x. 0 in Free (Ex (x. 3),(((x. 3) 'in' x) '&' ((H / (x. 0 ),y) / (x. 4),(x. 0 )))) ; :: thesis: x. 4 in Free H
then ( x. 0 in {(x. 3),x} \ {(x. 3)} or x. 0 in (Free ((H / (x. 0 ),y) / (x. 4),(x. 0 ))) \ {(x. 3)} ) by A6, XBOOLE_0:def 3;
then A15: ( x. 0 in {(x. 3),x} or x. 0 in Free ((H / (x. 0 ),y) / (x. 4),(x. 0 )) ) by XBOOLE_0:def 5;
A16: not x. 0 in variables_in (H / (x. 0 ),y) by A4, ZF_LANG1:198;

A17: now

assume not x. 4 in Free (H / (x. 0 ),y) ; :: thesis: contradiction
then A18: x. 0 in Free (H / (x. 0 ),y) by A3, A1, A15, A16, TARSKI:def 2, ZFMODEL2:2;
Free (H / (x. 0 ),y) c= variables_in (H / (x. 0 ),y) by ZF_LANG1:164;
hence contradiction by A4, A18, ZF_LANG1:198; :: thesis: verum

end;

Free (H / (x. 0 ),y) c= ((Free H) \ {(x. 0 )}) \/ {y} by ZFMODEL2:1;
then ( x. 4 in (Free H) \ {(x. 0 )} or x. 4 in {y} ) by A17, XBOOLE_0:def 3;
hence x. 4 in Free H by A5, TARSKI:def 1, XBOOLE_0:def 5; :: thesis: verum

end;

hence ( x. 4 in Free H iff x. 0 in Free (Ex (x. 3),(((x. 3) 'in' x) '&' ((H / (x. 0 ),y) / (x. 4),(x. 0 )))) ) by A8; :: thesis: verum