Axiom ax-addf 11219

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-order 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 11222 should be used. Note that uses of ax-addf 11219 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 11170. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)

Assertion

Ref	Expression
ax-addf	⊢ + :(ℂ × ℂ)⟶ℂ

Detailed syntax breakdown of Axiom ax-addf

Step	Hyp	Ref	Expression
1		cc 11138	. . 3 class ℂ
2	1, 1	cxp 5676	. 2 class (ℂ × ℂ)
3		caddc 11143	. 2 class +
4	2, 1, 3	wf 6545	1 wff + :(ℂ × ℂ)⟶ℂ

This axiom is referenced by:  addex  13006  rlimaddOLD  15624  cnfldadd  21302  dfcnfldOLD  21312  cnfldplusf  21341  addcn  24825  itg1addlem4  25672  itg1addlem4OLD  25673  cnaddabloOLD  30463  cnidOLD  30464  cncvcOLD  30465  cnnv  30559  cnnvba  30561  cncph  30701  raddcn  33661  addcomgi  44035