Description: Addition is an operation
on the complex numbers. This deprecated axiom is
provided for historical compatibility but is not a bona fide axiom for
complex numbers (independent of set theory) since it cannot be interpreted
as a first- or second-order statement (see
https://us.metamath.org/downloads/schmidt-cnaxioms.pdf).
It may be
deleted in the future and should be avoided for new theorems. Instead,
the less specific addcl 8004 should be used. Note that uses of ax-addf 8001 can
be eliminated by using the defined operation
         in place of , from which
this axiom (with the defined operation in place of ) follows as a
theorem.
This axiom is justified by Theorem axaddf 7935. (New usage is discouraged.)
(Contributed by NM, 19-Oct-2004.) |
