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: dom (H / x,x) = dom H by Def4;

now

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

end;

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