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:27;
hence x1 = x2 by A6, A9, QC_LANG2:5; :: thesis: verum