let A be QC-alphabet ; for x, y being bound_QC-variable of A
for p being Element of QC-WFF A st x <> y holds
(All (x,p)) . y = All (x,(p . y))
let x, y be bound_QC-variable of A; for p being Element of QC-WFF A st x <> y holds
(All (x,p)) . y = All (x,(p . y))
let p be Element of QC-WFF A; ( x <> y implies (All (x,p)) . y = All (x,(p . y)) )
set q = All (x,p);
A1:
All (x,p) is universal
by QC_LANG1:def 21;
then
( the_scope_of (All (x,p)) = p & bound_in (All (x,p)) = x )
by QC_LANG1:def 27, QC_LANG1:def 28;
hence
( x <> y implies (All (x,p)) . y = All (x,(p . y)) )
by A1, Th23; verum