Axiom ax-icn 7993

Description: i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 7949. (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 7900	. 2 class i
2		cc 7896	. 2 class ℂ
3	1, 2	wcel 2167	1 wff i ∈ ℂ

This axiom is referenced by:  0cn  8037  mulrid  8042  cnegexlem2  8221  cnegex  8223  0cnALT  8235  negicn  8246  ine0  8439  ixi  8629  rimul  8631  rereim  8632  apreap  8633  cru  8648  apreim  8649  mulreim  8650  apadd1  8654  apneg  8657  aprcl  8692  aptap  8696  recextlem1  8697  recexaplem2  8698  recexap  8699  crap0  9004  cju  9007  it0e0  9231  2mulicn  9232  iap0  9233  2muliap0  9234  cnref1o  9744  irec  10750  i2  10751  i3  10752  i4  10753  iexpcyc  10755  imval  11034  imre  11035  reim  11036  crre  11041  crim  11042  remim  11044  mulreap  11048  cjreb  11050  recj  11051  reneg  11052  readd  11053  remullem  11055  imcj  11059  imneg  11060  imadd  11061  cjadd  11068  cjneg  11074  imval2  11078  rei  11083  imi  11084  cji  11086  cjreim  11087  cjreim2  11088  cjap  11090  cnrecnv  11094  rennim  11186  absi  11243  absreimsq  11251  absreim  11252  absimle  11268  climcvg1nlem  11533  sinval  11886  cosval  11887  sinf  11888  cosf  11889  tanval2ap  11897  tanval3ap  11898  resinval  11899  recosval  11900  efi4p  11901  resin4p  11902  recos4p  11903  resincl  11904  recoscl  11905  sinneg  11910  cosneg  11911  efival  11916  efmival  11917  efeul  11918  sinadd  11920  cosadd  11921  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  absef  11954  absefib  11955  efieq1re  11956  demoivre  11957  demoivreALT  11958  igz  12570  4sqlem17  12603  cnrehmeocntop  14954  sincn  15113  coscn  15114  efhalfpi  15143  ef2kpi  15150  efper  15151  sinperlem  15152  efimpi  15163  2sqlem2  15464  qdencn  15784