theorem Th159: :: ZF_LANG1:159

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