let H be ZF-formula; :: thesis: for x, y being Variable st x <> y holds
not x in variables_in (H / (x,y))
let x, y be Variable; :: thesis: ( x <> y implies not x in variables_in (H / (x,y)) )
assume A1: x <> y ; :: thesis: not x in variables_in (H / (x,y))
assume x in variables_in (H / (x,y)) ; :: thesis: contradiction
then consider a being object such that
A2: a in dom (H / (x,y)) and
A3: x = (H / (x,y)) . a by FUNCT_1:def 3;
A4: dom (H / (x,y)) = dom H by Def3;
then ( H . a = x implies (H / (x,y)) . a = y ) by A2, Def3;
hence contradiction by A1, A2, A3, A4, Def3; :: thesis: verum