Axiom ax-addf 11263

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 11266 should be used. Note that uses of ax-addf 11263 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 11214. (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 11182	. . 3 class ℂ
2	1, 1	cxp 5698	. 2 class (ℂ × ℂ)
3		caddc 11187	. 2 class +
4	2, 1, 3	wf 6569	1 wff + :(ℂ × ℂ)⟶ℂ

This axiom is referenced by:  addex  13054  rlimaddOLD  15690  cnfldadd  21393  dfcnfldOLD  21403  cnfldplusf  21432  addcn  24906  itg1addlem4  25753  itg1addlem4OLD  25754  cnaddabloOLD  30613  cnidOLD  30614  cncvcOLD  30615  cnnv  30709  cnnvba  30711  cncph  30851  raddcn  33875  addcomgi  44425