let A be QC-alphabet ; :: thesis: 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; :: thesis: 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; :: thesis: ( p <==> q implies All (x,p) <==> All (x,q) )
assume A1: p <==> q ; :: thesis: 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; :: thesis: verum