theorem :: ZF_LANG1:20

for p, q being ZF-formula
for x, y, z, s, t being Variable st Ex (x,y,z,p) = Ex (t,s,q) holds
( x = t & y = s & Ex (z,p) = q )