let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in h holds
All (x,p) <==> All (y,q)
let p, q be Element of CQC-WFF A; :: thesis: for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in h holds
All (x,p) <==> All (y,q)
let h be QC-formula of A; :: thesis: for x, y being bound_QC-variable of A st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in h holds
All (x,p) <==> All (y,q)
let x, y be bound_QC-variable of A; :: thesis: ( p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in h implies All (x,p) <==> All (y,q) )
assume that
A1: p = h . x and
A2: q = h . y and
A3: not x in still_not-bound_in h and
A4: not y in still_not-bound_in h ; :: thesis: All (x,p) <==> All (y,q)

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: All (x,p) <==> All (y,q)

hence All (x,p) <==> All (y,q) by A1, A2; :: thesis: verum

end;

suppose A5: x <> y ; :: thesis: All (x,p) <==> All (y,q)

then not x in still_not-bound_in q by A2, A3, Th64;
then A6: (All (y,q)) => (All (x,p)) is valid by A1, A2, A4, CQC_THE2:27;
not y in still_not-bound_in p by A1, A4, A5, Th64;
then (All (x,p)) => (All (y,q)) is valid by A1, A2, A3, CQC_THE2:27;
hence All (x,p) <==> All (y,q) by A6, Th50; :: thesis: verum

end;

end;