let H be ZF-formula; :: thesis: for x, y, z being Variable st x <> y holds
(H / (x,y)) / (x,z) = H / (x,y)
let x, y, z be Variable; :: thesis: ( x <> y implies (H / (x,y)) / (x,z) = H / (x,y) )
assume x <> y ; :: thesis: (H / (x,y)) / (x,z) = H / (x,y)
then not x in variables_in (H / (x,y)) by Th184;
hence (H / (x,y)) / (x,z) = H / (x,y) by Th182; :: thesis: verum