Axiom ax-icn 6979

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

This axiom is referenced by:  0cn  7019  mulid1  7024  cnegexlem2  7187  cnegex  7189  0cnALT  7201  negicn  7212  ine0  7391  ixi  7574  rimul  7576  rereim  7577  apreap  7578  cru  7593  apreim  7594  mulreim  7595  apadd1  7599  apneg  7602  recextlem1  7632  recexaplem2  7633  recexap  7634  crap0  7910  cju  7913  it0e0  8146  2mulicn  8147  iap0  8148  2muliap0  8149  cnref1o  8582  irec  9352  i2  9353  i3  9354  i4  9355  imval  9450  imre  9451  reim  9452  crre  9457  crim  9458  remim  9460  mulreap  9464  cjreb  9466  recj  9467  reneg  9468  readd  9469  remullem  9471  imcj  9475  imneg  9476  imadd  9477  cjadd  9484  cjneg  9490  imval2  9494  rei  9499  imi  9500  cji  9502  cjreim  9503  cjreim2  9504  cjap  9506  cnrecnv  9510  rennim  9600  absi  9657  absreimsq  9665  absreim  9666  absimle  9680  climcvg1nlem  9868  qdencn  10124