Axiom ax-icn 6758

Description: i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 6729. (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 6693	. 2 class i
2		cc 6689	. 2 class ℂ
3	1, 2	wcel 1390	1 wff i ∈ ℂ

This axiom is referenced by:  0cn  6797  mulid1  6802  cnegexlem2  6964  cnegex  6966  0cnALT  6978  negicn  6989  ine0  7167  ixi  7347  rimul  7349  rereim  7350  apreap  7351  cru  7366  apreim  7367  mulreim  7368  apadd1  7372  apneg  7375  recextlem1  7394  recexaplem2  7395  recexap  7396  crap0  7671  cju  7674  it0e0  7903  2mulicn  7904  iap0  7905  2muliap0  7906  cnref1o  8337  irec  8985  i2  8986  i3  8987  i4  8988  imval  9058  imre  9059  reim  9060  crre  9065  crim  9066  remim  9068  mulreap  9072  cjreb  9074  recj  9075  reneg  9076  readd  9077  remullem  9079  imcj  9083  imneg  9084  imadd  9085  cjadd  9092  cjneg  9098  imval2  9102  rei  9107  imi  9108  cji  9110  cjreim  9111  cjreim2  9112  cjap  9114  cnrecnv  9118  rennim  9191  absi  9203