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 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 ) & 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
then consider B1 being Element of [:QC-Sub-WFF ,bound_QC-variables :], SQ1 being second_Q_comp of B1 such that
A4: ( A = Sub_All B1,SQ1 & B1 `2 = x1 & B1 is quantifiable ) ;
consider B2 being Element of [:QC-Sub-WFF ,bound_QC-variables :], SQ2 being second_Q_comp of B2 such that
A5: ( A = Sub_All B2,SQ2 & B2 `2 = x2 & B2 is quantifiable ) by A3;
A6: [(All (B1 `2 ),((B1 `1 ) `1 )),SQ1] = A by A4, Def24;
[(All (B2 `2 ),((B2 `1 ) `1 )),SQ2] = A by A5, Def24;
then All (B1 `2 ),((B1 `1 ) `1 ) = All (B2 `2 ),((B2 `1 ) `1 ) by A6, ZFMISC_1:33;
hence x1 = x2 by A4, A5, QC_LANG2:6; :: thesis: verum