let x, y be Variable; :: thesis: for G, H being ZF-formula st Ex (x,H) = Ex (y,G) holds
( x = y & H = G )
let G, H be ZF-formula; :: thesis: ( Ex (x,H) = Ex (y,G) implies ( x = y & H = G ) )
assume Ex (x,H) = Ex (y,G) ; :: thesis: ( x = y & H = G )
then A1: All (x,('not' H)) = All (y,('not' G)) by FINSEQ_1:33;
then 'not' H = 'not' G by Th3;
hence ( x = y & H = G ) by A1, Th3, FINSEQ_1:33; :: thesis: verum