let H be ZF-formula; :: thesis: for x, y being Variable st not x in variables_in H holds
H / x,y = H
let x, y be Variable; :: thesis: ( not x in variables_in H implies H / x,y = H )
assume not x in variables_in H ; :: thesis: H / x,y = H
then A1: ( not x in (rng H) \ {0 ,1,2,3,4} & not x in {0 ,1,2,3,4} ) by Th149;
then A2: ( not x in rng H & dom H = dom (H / x,y) ) by Def4, XBOOLE_0:def 5;

now

let a be set ; :: thesis: ( a in dom H implies (H / x,y) . a = H . a )
assume a in dom H ; :: thesis: (H / x,y) . a = H . a
then ( H . a in rng H & ( H . a <> x implies (H / x,y) . a = H . a ) ) by Def4, FUNCT_1:def 5;
hence (H / x,y) . a = H . a by A1, XBOOLE_0:def 5; :: thesis: verum

end;

hence H / x,y = H by A2, FUNCT_1:9; :: thesis: verum