let p1, p2 be ZF-formula; :: thesis: for x1, x2, y1, y2, z1, z2 being Variable st Ex (x1,y1,z1,p1) = Ex (x2,y2,z2,p2) holds
( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
let x1, x2, y1, y2, z1, z2 be Variable; :: thesis: ( Ex (x1,y1,z1,p1) = Ex (x2,y2,z2,p2) implies ( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 ) )
assume A1: Ex (x1,y1,z1,p1) = Ex (x2,y2,z2,p2) ; :: thesis: ( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
then Ex (y1,z1,p1) = Ex (y2,z2,p2) by ZF_LANG:34;
hence ( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 ) by A1, Th17, ZF_LANG:34; :: thesis: verum