MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-addf Unicode version

Axiom ax-addf 9058
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 http://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 9061 should be used. Note that uses of ax-addf 9058 can be eliminated by using the defined operation  ( x  e.  CC ,  y  e.  CC  |->  ( x  +  y ) ) 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 9009. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)

Assertion
Ref Expression
ax-addf  |-  +  :
( CC  X.  CC )
--> CC

Detailed syntax breakdown of Axiom ax-addf
StepHypRef Expression
1 cc 8977 . . 3  class  CC
21, 1cxp 4867 . 2  class  ( CC 
X.  CC )
3 caddc 8982 . 2  class  +
42, 1, 3wf 5441 1  wff  +  :
( CC  X.  CC )
--> CC
Colors of variables: wff set class
This axiom is referenced by:  addex  10599  rlimadd  12424  cnfldplusf  16716  addcn  18883  itg1addlem4  19579  cnaddablo  21926  cnid  21927  addinv  21928  readdsubgo  21929  zaddsubgo  21930  efghgrp  21949  cnrngo  21979  cncvc  22050  cnnv  22156  cnnvba  22158  cncph  22308  raddcn  24303  addcomgi  27575
  Copyright terms: Public domain W3C validator