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

Axiom ax-addf 9069
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 9072 should be used. Note that uses of ax-addf 9069 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 9020. (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 8988 . . 3  class  CC
21, 1cxp 4876 . 2  class  ( CC 
X.  CC )
3 caddc 8993 . 2  class  +
42, 1, 3wf 5450 1  wff  +  :
( CC  X.  CC )
--> CC
Colors of variables: wff set class
This axiom is referenced by:  addex  10610  rlimadd  12436  cnfldplusf  16728  addcn  18895  itg1addlem4  19591  cnaddablo  21938  cnid  21939  addinv  21940  readdsubgo  21941  zaddsubgo  21942  efghgrp  21961  cnrngo  21991  cncvc  22062  cnnv  22168  cnnvba  22170  cncph  22320  raddcn  24315  addcomgi  27637
  Copyright terms: Public domain W3C validator