Axiom ax-icn 7906

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

This axiom is referenced by:  0cn  7949  mulrid  7954  cnegexlem2  8133  cnegex  8135  0cnALT  8147  negicn  8158  ine0  8351  ixi  8540  rimul  8542  rereim  8543  apreap  8544  cru  8559  apreim  8560  mulreim  8561  apadd1  8565  apneg  8568  aprcl  8603  aptap  8607  recextlem1  8608  recexaplem2  8609  recexap  8610  crap0  8915  cju  8918  it0e0  9140  2mulicn  9141  iap0  9142  2muliap0  9143  cnref1o  9650  irec  10620  i2  10621  i3  10622  i4  10623  iexpcyc  10625  imval  10859  imre  10860  reim  10861  crre  10866  crim  10867  remim  10869  mulreap  10873  cjreb  10875  recj  10876  reneg  10877  readd  10878  remullem  10880  imcj  10884  imneg  10885  imadd  10886  cjadd  10893  cjneg  10899  imval2  10903  rei  10908  imi  10909  cji  10911  cjreim  10912  cjreim2  10913  cjap  10915  cnrecnv  10919  rennim  11011  absi  11068  absreimsq  11076  absreim  11077  absimle  11093  climcvg1nlem  11357  sinval  11710  cosval  11711  sinf  11712  cosf  11713  tanval2ap  11721  tanval3ap  11722  resinval  11723  recosval  11724  efi4p  11725  resin4p  11726  recos4p  11727  resincl  11728  recoscl  11729  sinneg  11734  cosneg  11735  efival  11740  efmival  11741  efeul  11742  sinadd  11744  cosadd  11745  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  absef  11777  absefib  11778  efieq1re  11779  demoivre  11780  demoivreALT  11781  igz  12372  cnrehmeocntop  14096  sincn  14193  coscn  14194  efhalfpi  14223  ef2kpi  14230  efper  14231  sinperlem  14232  efimpi  14243  2sqlem2  14465  qdencn  14778