let H be ZF-formula; :: thesis: for x, y being Variable st not x in variables_in H & 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 x, y be Variable; :: thesis: ( not x in variables_in H & 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 )))) ) )
assume A1: ( not x in variables_in H & not y in variables_in H & x <> x. 0 & y <> x. 0 & 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 )))) )
A2: ( x. 0 <> x. 3 & x. 0 <> x. 4 ) by ZF_LANG1:86;
set G = (H / (x. 0 ),y) / (x. 4),(x. 0 );
A3: 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 ;

A4: now

assume A5: 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 ))))
A6: 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 x. 0 in Free H ; :: thesis: x. 4 in Free (H / (x. 0 ),y)

then A7: Free (H / (x. 0 ),y) = ((Free H) \ {(x. 0 )}) \/ {y} by A1, ZFMODEL2:2;
not x. 4 in {(x. 0 )} by A2, TARSKI:def 1;
then x. 4 in (Free H) \ {(x. 0 )} by A5, XBOOLE_0:def 5;
hence x. 4 in Free (H / (x. 0 ),y) by A7, 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 A1, A5, ZFMODEL2:2; :: thesis: verum

end;

end;

end;

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

end;

not x. 0 in variables_in (H / (x. 0 ),y) by A1, ZF_LANG1:198;
then A8: Free ((H / (x. 0 ),y) / (x. 4),(x. 0 )) = ((Free (H / (x. 0 ),y)) \ {(x. 4)}) \/ {(x. 0 )} by A6, ZFMODEL2:2;
x. 0 in {(x. 0 )} by TARSKI:def 1;
then ( x. 0 in Free ((H / (x. 0 ),y) / (x. 4),(x. 0 )) & not x. 0 in {(x. 3)} ) by A2, A8, TARSKI:def 1, XBOOLE_0:def 3;
then x. 0 in (Free ((H / (x. 0 ),y) / (x. 4),(x. 0 ))) \ {(x. 3)} by 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 A3, 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 A3, XBOOLE_0:def 3;
then A9: ( x. 0 in {(x. 3),x} or x. 0 in Free ((H / (x. 0 ),y) / (x. 4),(x. 0 )) ) by XBOOLE_0:def 5;
A10: not x. 0 in variables_in (H / (x. 0 ),y) by A1, ZF_LANG1:198;

A11: now

assume not x. 4 in Free (H / (x. 0 ),y) ; :: thesis: contradiction
then A12: x. 0 in Free (H / (x. 0 ),y) by A1, A2, A9, A10, TARSKI:def 2, ZFMODEL2:2;
Free (H / (x. 0 ),y) c= variables_in (H / (x. 0 ),y) by ZF_LANG1:164;
hence contradiction by A1, A12, 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 A11, XBOOLE_0:def 3;
hence x. 4 in Free H by A1, 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 A4; :: thesis: verum