let p, q be ZF-formula; :: thesis: 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 )
let x, y, z, s, t be Variable; :: thesis: ( Ex (x,y,z,p) = Ex (t,s,q) implies ( x = t & y = s & Ex (z,p) = q ) )
Ex (x,y,z,p) = Ex (x,y,(Ex (z,p))) ;
hence ( Ex (x,y,z,p) = Ex (t,s,q) implies ( x = t & y = s & Ex (z,p) = q ) ) by Th17; :: thesis: verum