A2: now :: thesis: for x being bound_QC-variable of F1()
for S being Element of QC-Sub-WFF F1()
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds
P1[ Sub_All ([S,x],SQ)]
let x be bound_QC-variable of F1(); :: thesis: for S being Element of QC-Sub-WFF F1()
for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds
P1[ Sub_All ([S,x],SQ)]
let S be Element of QC-Sub-WFF F1(); :: thesis: for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds
P1[ Sub_All ([S,x],SQ)]
let SQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable & P1[S] implies P1[ Sub_All ([S,x],SQ)] )
assume that
A3: [S,x] is quantifiable and
A4: P1[S] ; :: thesis: P1[ Sub_All ([S,x],SQ)]
[S,x] `1 = Sub_the_scope_of (Sub_All ([S,x],SQ)) by A3, Th21;
then A5: S = Sub_the_scope_of (Sub_All ([S,x],SQ)) ;
Sub_All ([S,x],SQ) is Sub_universal by A3;
hence P1[ Sub_All ([S,x],SQ)] by A1, A4, A5; :: thesis: verum
end;
A6: now :: thesis: for S1, S2 being Element of QC-Sub-WFF F1() st S1 `2 = S2 `2 & P1[S1] & P1[S2] holds
P1[ Sub_& (S1,S2)]
let S1, S2 be Element of QC-Sub-WFF F1(); :: thesis: ( S1 `2 = S2 `2 & P1[S1] & P1[S2] implies P1[ Sub_& (S1,S2)] )
assume that
A7: S1 `2 = S2 `2 and
A8: ( P1[S1] & P1[S2] ) ; :: thesis: P1[ Sub_& (S1,S2)]
A9: S2 = Sub_the_right_argument_of (Sub_& (S1,S2)) by A7, Th19;
( Sub_& (S1,S2) is Sub_conjunctive & S1 = Sub_the_left_argument_of (Sub_& (S1,S2)) ) by A7, Th18;
hence P1[ Sub_& (S1,S2)] by A1, A8, A9; :: thesis: verum
end;
A10: now :: thesis: for S being Element of QC-Sub-WFF F1() st P1[S] holds
P1[ Sub_not S]
let S be Element of QC-Sub-WFF F1(); :: thesis: ( P1[S] implies P1[ Sub_not S] )
assume A11: P1[S] ; :: thesis: P1[ Sub_not S]
S = Sub_the_argument_of (Sub_not S) by Def30;
hence P1[ Sub_not S] by A1, A11; :: thesis: verum
end;
A12: for S being Element of QC-Sub-WFF F1() st S is F1() -Sub_VERUM holds
P1[S] by A1;
A13: for k being Nat
for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1()
for e being Element of vSUB F1() holds P1[ Sub_P (P,ll,e)] by A1;
thus for S being Element of QC-Sub-WFF F1() holds P1[S] from SUBSTUT1:sch 1(A13, A12, A10, A6, A2); :: thesis: verum