Axiom ax-icn 6738

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

This axiom is referenced by:  0cn  6777  mulid1  6782  cnegexlem2  6944  cnegex  6946  0cnALT  6958  negicn  6969  ine0  7147  ixi  7327  rimul  7329  rereim  7330  apreap  7331  cru  7346  apreim  7347  mulreim  7348  apadd1  7352  apneg  7355  recextlem1  7374  recexaplem2  7375  recexap  7376  crap0  7651  cju  7654  it0e0  7883  2mulicn  7884  iap0  7885  2muliap0  7886  cnref1o  8317  irec  8965  i2  8966  i3  8967  i4  8968  imval  9038  imre  9039  reim  9040  crre  9045  crim  9046  remim  9048  mulreap  9052  cjreb  9054  recj  9055  reneg  9056  readd  9057  remullem  9059  imcj  9063  imneg  9064  imadd  9065  cjadd  9072  cjneg  9078  imval2  9082  rei  9087  imi  9088  cji  9090  cjreim  9091  cjreim2  9092  cjap  9094  cnrecnv  9098