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