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

Axiom ax-addf 8816
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 8819 should be used. Note that uses of ax-addf 8816 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 8767. (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 8735 . . 3  class  CC
21, 1cxp 4687 . 2  class  ( CC 
X.  CC )
3 caddc 8740 . 2  class  +
42, 1, 3wf 5251 1  wff  +  :
( CC  X.  CC )
--> CC
Colors of variables: wff set class
This axiom is referenced by:  addex  10352  rlimadd  12116  cnfldplusf  16401  addcn  18369  itg1addlem4  19054  cnaddablo  21017  cnid  21018  addinv  21019  readdsubgo  21020  zaddsubgo  21021  efghgrp  21040  cnrngo  21070  cncvc  21139  cnnv  21245  cnnvba  21247  cncph  21397  raddcn  23302  zintdom  25438  addcomgi  27661
  Copyright terms: Public domain W3C validator