let H be ZF-formula; for x, y being Variable holds variables_in (H / (x,y)) c= ((variables_in H) \ {x}) \/ {y}
let x, y be Variable; variables_in (H / (x,y)) c= ((variables_in H) \ {x}) \/ {y}
let a be object ; TARSKI:def 3 ( not a in variables_in (H / (x,y)) or a in ((variables_in H) \ {x}) \/ {y} )
assume A1:
a in variables_in (H / (x,y))
; a in ((variables_in H) \ {x}) \/ {y}
then reconsider z = a as Variable ;
consider b being object such that
A2:
b in dom (H / (x,y))
and
A3:
z = (H / (x,y)) . b
by A1, FUNCT_1:def 3;
A4:
dom (H / (x,y)) = dom H
by Def3;
then A5:
( H . b <> x implies z = H . b )
by A2, A3, Def3;
( H . b = x implies z = y )
by A2, A3, A4, Def3;
then
( z in {y} or ( z in rng H & not z in {0,1,2,3,4} & not z in {x} ) )
by A2, A4, A5, Th136, FUNCT_1:def 3, TARSKI:def 1;
then
( z in {y} or ( z in (rng H) \ {0,1,2,3,4} & not z in {x} ) )
by XBOOLE_0:def 5;
then
( z in {y} or z in (variables_in H) \ {x} )
by XBOOLE_0:def 5;
hence
a in ((variables_in H) \ {x}) \/ {y}
by XBOOLE_0:def 3; verum