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 :: thesis: for a being object st a in dom H holds
H . a = (H / (x,x)) . a
let a be object ; :: 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 Def3;
hence H . a = (H / (x,x)) . a by A2, Def3; :: thesis: verum
end;
dom (H / (x,x)) = dom H by Def3;
hence H / (x,x) = H by A1, FUNCT_1:2; :: thesis: verum