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:9; :: thesis: verum