A2:
now 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();
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();
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];
( [S,x] is quantifiable & P1[S] implies P1[ Sub_All ([S,x],SQ)] )assume that A3:
[S,x] is
quantifiable
and A4:
P1[
S]
;
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;
verum end;
A6:
now 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();
( 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] )
;
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;
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); verum