let A be QC-alphabet ; 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; 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; 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; ( 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
; All (x,p) <==> All (y,q)
per cases
( x = y or x <> y )
;
suppose A5:
x <> y
;
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;
verum end; end;