theorem Th160: :: ZF_LANG1:160

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