ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-addf GIF version

Axiom ax-addf 7754
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 It may be deleted in the future and should be avoided for new theorems. Instead, the less specific addcl 7757 should be used. Note that uses of ax-addf 7754 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 7688. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)

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

Detailed syntax breakdown of Axiom ax-addf
StepHypRef Expression
1 cc 7630 . . 3 class
21, 1cxp 4537 . 2 class (ℂ × ℂ)
3 caddc 7635 . 2 class +
42, 1, 3wf 5119 1 wff + :(ℂ × ℂ)⟶ℂ
Colors of variables: wff set class
This axiom is referenced by:  addcncntop  12735
  Copyright terms: Public domain W3C validator