let p, q be ZF-formula; :: thesis: for x, y, z, t, s 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, t, s 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 Th20; :: thesis: verum