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