let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A holds (All (x,p)) . x = All (x,p)
let x be bound_QC-variable of A; :: thesis: for p being Element of QC-WFF A holds (All (x,p)) . x = All (x,p)
let p be Element of QC-WFF A; :: thesis: (All (x,p)) . x = All (x,p)
set q = All (x,p);
A1: All (x,p) is universal by QC_LANG1:def 21;
then bound_in (All (x,p)) = x by QC_LANG1:def 27;
hence (All (x,p)) . x = All (x,p) by A1, Th22; :: thesis: verum