Axiom ax-icn 6778

Description: i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 6749. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-icn	⊢ i ∈ ℂ

Detailed syntax breakdown of Axiom ax-icn

Step	Hyp	Ref	Expression
1		ci 6713	. 2 class i
2		cc 6709	. 2 class ℂ
3	1, 2	wcel 1390	1 wff i ∈ ℂ

This axiom is referenced by:  0cn  6817  mulid1  6822  cnegexlem2  6984  cnegex  6986  0cnALT  6998  negicn  7009  ine0  7187  ixi  7367  rimul  7369  rereim  7370  apreap  7371  cru  7386  apreim  7387  mulreim  7388  apadd1  7392  apneg  7395  recextlem1  7414  recexaplem2  7415  recexap  7416  crap0  7691  cju  7694  it0e0  7923  2mulicn  7924  iap0  7925  2muliap0  7926  cnref1o  8357  irec  9005  i2  9006  i3  9007  i4  9008  imval  9078  imre  9079  reim  9080  crre  9085  crim  9086  remim  9088  mulreap  9092  cjreb  9094  recj  9095  reneg  9096  readd  9097  remullem  9099  imcj  9103  imneg  9104  imadd  9105  cjadd  9112  cjneg  9118  imval2  9122  rei  9127  imi  9128  cji  9130  cjreim  9131  cjreim2  9132  cjap  9134  cnrecnv  9138  rennim  9211  absi  9223