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 A1: All (x,('not' p)) = All (y,('not' q)) by FINSEQ_1:33;
then 'not' p = 'not' q by Th6;
hence ( x = y & p = q ) by A1, Th6, FINSEQ_1:33; :: thesis: verum