let H be ZF-formula; for x, y being Variable st not x in variables_in H holds
H / (x,y) = H
let x, y be Variable; ( not x in variables_in H implies H / (x,y) = H )
assume A1:
not x in variables_in H
; H / (x,y) = H
A2:
not x in {0,1,2,3,4}
by Th136;
dom H = dom (H / (x,y))
by Def3;
hence
H / (x,y) = H
by A3, FUNCT_1:2; verum