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 A1: not x in variables_in H ; :: thesis: H / x,y = H
A2: not x in {0 ,1,2,3,4} by Th149;

A3: now

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

end;

dom H = dom (H / x,y) by Def4;
hence H / x,y = H by A3, FUNCT_1:9; :: thesis: verum