A2: for x being bound_QC-variable
for S being Element of CQC-Sub-WFF
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 x be bound_QC-variable; :: thesis: for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds
P1[ Sub_All [S,x],xSQ]
let S be Element of CQC-Sub-WFF ; :: 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]
CQCSub_All [S,x],xSQ = Sub_All [S,x],xSQ by A3, Def6;
hence P1[ Sub_All [S,x],xSQ] by A1, A3, A4; :: thesis: verum
end;
for S, S9 being Element of CQC-Sub-WFF st S `2 = S9 `2 & P1[S] & P1[S9] holds
P1[ Sub_& S,S9]
proof
let S, S9 be Element of CQC-Sub-WFF ; :: 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, Def4;
hence P1[ Sub_& S,S9] by A1, A5, A6; :: thesis: verum
end;
then A7: for S, S9 being Element of CQC-Sub-WFF
for x being bound_QC-variable
for SQ being second_Q_comp of [S,x]
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k
for e being Element of vSUB holds
( P1[ Sub_P P,ll,e] & ( S is 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 holds P1[S] from SUBSTUT1:sch 5(A7); :: thesis: verum