A2: for S, S9 being Element of CQC-Sub-WFF F1()
for x being bound_QC-variable of F1()
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds
P1[ Sub_All ([S,x],xSQ)]
proof
let S, S9 be Element of CQC-Sub-WFF F1(); :: thesis: for x being bound_QC-variable of F1()
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds
P1[ Sub_All ([S,x],xSQ)]
let x be bound_QC-variable of F1(); :: thesis: for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds
P1[ Sub_All ([S,x],xSQ)]
let xSQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable & P1[S] implies P1[ Sub_All ([S,x],xSQ)] )
assume that
A3: [S,x] is quantifiable and
A4: P1[S] ; :: thesis: P1[ Sub_All ([S,x],xSQ)]
P1[ CQCSub_All ([S,x],xSQ)] by A1, A3, A4;
hence P1[ Sub_All ([S,x],xSQ)] by A3, Def5; :: thesis: verum
end;
for S, S9 being Element of CQC-Sub-WFF F1() st S `2 = S9 `2 & P1[S] & P1[S9] holds
P1[ Sub_& (S,S9)]
proof
let S, S9 be Element of CQC-Sub-WFF F1(); :: thesis: ( S `2 = S9 `2 & P1[S] & P1[S9] implies P1[ Sub_& (S,S9)] )
assume that
A5: S `2 = S9 `2 and
A6: ( P1[S] & P1[S9] ) ; :: thesis: P1[ Sub_& (S,S9)]
CQCSub_& (S,S9) = Sub_& (S,S9) by A5, Def3;
hence P1[ Sub_& (S,S9)] by A1, A5, A6; :: thesis: verum
end;
then A7: for S, S9 being Element of CQC-Sub-WFF F1()
for x being bound_QC-variable of F1()
for SQ being second_Q_comp of [S,x]
for k being Nat
for ll being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1()
for e being Element of vSUB F1() holds
( P1[ Sub_P (P,ll,e)] & ( S is F1() -Sub_VERUM implies P1[S] ) & ( P1[S] implies P1[ Sub_not S] ) & ( S `2 = S9 `2 & P1[S] & P1[S9] implies P1[ Sub_& (S,S9)] ) & ( [S,x] is quantifiable & P1[S] implies P1[ Sub_All ([S,x],SQ)] ) ) by A1, A2;
thus for S being Element of CQC-Sub-WFF F1() holds P1[S] from SUBSTUT1:sch 5(A7); :: thesis: verum