let H be ZF-formula; for x, y, z being Variable st x <> y holds
(H / (x,y)) / (x,z) = H / (x,y)
let x, y, z be Variable; ( x <> y implies (H / (x,y)) / (x,z) = H / (x,y) )
assume
x <> y
; (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; verum