let H be ZF-formula; :: thesis: for x being Variable holds H / (x,x) = H
let x be Variable; :: thesis: H / (x,x) = H

A1: now

let a be set ; :: thesis: ( a in dom H implies H . a = (H / (x,x)) . a )
assume A2: a in dom H ; :: thesis: H . a = (H / (x,x)) . a
then ( H . a = x implies (H / (x,x)) . a = x ) by Def4;
hence H . a = (H / (x,x)) . a by A2, Def4; :: thesis: verum

end;

dom (H / (x,x)) = dom H by Def4;
hence H / (x,x) = H by A1, FUNCT_1:2; :: thesis: verum