let x, y be Variable; :: thesis: for H, G being ZF-formula st Ex (x,H) = Ex (y,G) holds
( x = y & H = G )
let H, G 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 Th12;
hence ( x = y & H = G ) by A1, Th12, FINSEQ_1:33; :: thesis: verum