theorem Th34: :: ZF_LANG:34

for x, y being Variable
for G, H being ZF-formula st Ex (x,H) = Ex (y,G) holds
( x = y & H = G )