let x, y be bound_QC-variable; :: thesis: for p, q being Element of QC-WFF st Ex x,p = Ex y,q holds
( x = y & p = q )
let p, q be Element of QC-WFF ; :: thesis: ( Ex x,p = Ex y,q implies ( x = y & p = q ) )
assume Ex x,p = Ex y,q ; :: thesis: ( x = y & p = q )
then All x,('not' p) = All y,('not' q) by FINSEQ_1:46;
then ( x = y & 'not' p = 'not' q ) by Th6;
hence ( x = y & p = q ) by FINSEQ_1:46; :: thesis: verum