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:46;
then 'not' H = 'not' G by Th12;
hence ( x = y & H = G ) by A1, Th12, FINSEQ_1:46; :: thesis: verum