theorem Th165: :: ZF_LANG1:165

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