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

Axiom ax-addf 9025
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 9028 should be used. Note that uses of ax-addf 9025 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 8976. (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 8944 . . 3  class  CC
21, 1cxp 4835 . 2  class  ( CC 
X.  CC )
3 caddc 8949 . 2  class  +
42, 1, 3wf 5409 1  wff  +  :
( CC  X.  CC )
--> CC
Colors of variables: wff set class
This axiom is referenced by:  addex  10566  rlimadd  12391  cnfldplusf  16683  addcn  18848  itg1addlem4  19544  cnaddablo  21891  cnid  21892  addinv  21893  readdsubgo  21894  zaddsubgo  21895  efghgrp  21914  cnrngo  21944  cncvc  22015  cnnv  22121  cnnvba  22123  cncph  22273  raddcn  24268  addcomgi  27528
  Copyright terms: Public domain W3C validator