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

Axiom ax-addf 8903
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 8906 should be used. Note that uses of ax-addf 8903 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 8854. (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 8822 . . 3  class  CC
21, 1cxp 4766 . 2  class  ( CC 
X.  CC )
3 caddc 8827 . 2  class  +
42, 1, 3wf 5330 1  wff  +  :
( CC  X.  CC )
--> CC
Colors of variables: wff set class
This axiom is referenced by:  addex  10441  rlimadd  12206  cnfldplusf  16501  addcn  18466  itg1addlem4  19152  cnaddablo  21123  cnid  21124  addinv  21125  readdsubgo  21126  zaddsubgo  21127  efghgrp  21146  cnrngo  21176  cncvc  21247  cnnv  21353  cnnvba  21355  cncph  21505  raddcn  23471  addcomgi  26984
  Copyright terms: Public domain W3C validator