theorem :: ZF_LANG1:186

for H being ZF-formula
for x, y, z being Variable st x <> y holds
(H / (x,y)) / (x,z) = H / (x,y)