let Al be QC-alphabet ; for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
S `2 = ExpandSub (x,(S `1),(RestrictSub (x,(All (x,(S `1))),xSQ)))
let x be bound_QC-variable of Al; for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
S `2 = ExpandSub (x,(S `1),(RestrictSub (x,(All (x,(S `1))),xSQ)))
let S be Element of CQC-Sub-WFF Al; for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
S `2 = ExpandSub (x,(S `1),(RestrictSub (x,(All (x,(S `1))),xSQ)))
let xSQ be second_Q_comp of [S,x]; ( [S,x] is quantifiable implies S `2 = ExpandSub (x,(S `1),(RestrictSub (x,(All (x,(S `1))),xSQ))) )
set Z = [(All (x,(S `1))),xSQ];
set q = All (x,(S `1));
assume
[S,x] is quantifiable
; S `2 = ExpandSub (x,(S `1),(RestrictSub (x,(All (x,(S `1))),xSQ)))
then A1:
([S,x] `1) `2 = (QSub Al) . [(All (([S,x] `2),(([S,x] `1) `1))),xSQ]
by SUBSTUT1:def 23;
A2:
[(All (x,(S `1))),xSQ] in [:(QC-WFF Al),(vSUB Al):]
by ZFMISC_1:def 2;
[:(QC-WFF Al),(vSUB Al):] c= dom (QSub Al)
by Th34;
then
[[(All (x,(S `1))),xSQ],(([S,x] `1) `2)] in QSub Al
by A2, A1, FUNCT_1:1;
then
[[(All (x,(S `1))),xSQ],(S `2)] in QSub Al
;
then consider p being QC-formula of Al, Sub1 being CQC_Substitution of Al, b being object such that
A3:
[[(All (x,(S `1))),xSQ],(S `2)] = [[p,Sub1],b]
and
A4:
p,Sub1 PQSub b
by SUBSTUT1:def 15;
[(All (x,(S `1))),xSQ] = [p,Sub1]
by A3, XTUPLE_0:1;
then A5:
( All (x,(S `1)) = p & xSQ = Sub1 )
by XTUPLE_0:1;
A6:
All (x,(S `1)) is universal
by QC_LANG1:def 21;
then A7:
bound_in (All (x,(S `1))) = x
by QC_LANG1:def 27;
S `2 = b
by A3, XTUPLE_0:1;
then
S `2 = ExpandSub ((bound_in (All (x,(S `1)))),(the_scope_of (All (x,(S `1)))),(RestrictSub ((bound_in (All (x,(S `1)))),(All (x,(S `1))),xSQ)))
by A4, A5, A6, SUBSTUT1:def 14;
hence
S `2 = ExpandSub (x,(S `1),(RestrictSub (x,(All (x,(S `1))),xSQ)))
by A6, A7, QC_LANG1:def 28; verum