let p1, p2 be ZF-formula; 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; ( 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)
; ( 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; verum