let x1, x2 be bound_QC-variable; :: thesis: ( ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `2 = x1 & B is quantifiable ) & ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `2 = x2 & B is quantifiable ) implies x1 = x2 )
assume that
A3: ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `2 = x1 & B is quantifiable ) and
A4: ex B being Element of [:QC-Sub-WFF ,bound_QC-variables :] ex SQ being second_Q_comp of B st
( A = Sub_All B,SQ & B `2 = x2 & B is quantifiable ) ; :: thesis: x1 = x2
consider B1 being Element of [:QC-Sub-WFF ,bound_QC-variables :], SQ1 being second_Q_comp of B1 such that
A5: A = Sub_All B1,SQ1 and
A6: B1 `2 = x1 and
A7: B1 is quantifiable by A3;
consider B2 being Element of [:QC-Sub-WFF ,bound_QC-variables :], SQ2 being second_Q_comp of B2 such that
A8: A = Sub_All B2,SQ2 and
A9: B2 `2 = x2 and
A10: B2 is quantifiable by A4;
A11: [(All (B2 `2 ),((B2 `1 ) `1 )),SQ2] = A by A8, A10, Def24;
[(All (B1 `2 ),((B1 `1 ) `1 )),SQ1] = A by A5, A7, Def24;
then All (B1 `2 ),((B1 `1 ) `1 ) = All (B2 `2 ),((B2 `1 ) `1 ) by A11, ZFMISC_1:33;
hence x1 = x2 by A6, A9, QC_LANG2:6; :: thesis: verum