let A be QC-alphabet ; for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st p <==> q holds
All (x,p) <==> All (x,q)
let p, q be Element of CQC-WFF A; for x being bound_QC-variable of A st p <==> q holds
All (x,p) <==> All (x,q)
let x be bound_QC-variable of A; ( p <==> q implies All (x,p) <==> All (x,q) )
assume A1:
p <==> q
; All (x,p) <==> All (x,q)
then
q => p is valid
by Th50;
then
All (x,(q => p)) is valid
by CQC_THE2:23;
then A2:
(All (x,q)) => (All (x,p)) is valid
by CQC_THE2:31;
p => q is valid
by A1, Th50;
then
All (x,(p => q)) is valid
by CQC_THE2:23;
then
(All (x,p)) => (All (x,q)) is valid
by CQC_THE2:31;
hence
All (x,p) <==> All (x,q)
by A2, Th50; verum