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 set such that
A2: ( a in dom (H / x,y) & x = (H / x,y) . a ) by FUNCT_1:def 5;
dom (H / x,y) = dom H by Def4;
then ( ( H . a = x implies (H / x,y) . a = y ) & ( H . a <> x implies (H / x,y) . a = H . a ) ) by A2, Def4;
hence contradiction by A1, A2; :: thesis: verum