Axiom ax-icn 8090

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

This axiom is referenced by:  0cn  8134  mulrid  8139  cnegexlem2  8318  cnegex  8320  0cnALT  8332  negicn  8343  ine0  8536  ixi  8726  rimul  8728  rereim  8729  apreap  8730  cru  8745  apreim  8746  mulreim  8747  apadd1  8751  apneg  8754  aprcl  8789  aptap  8793  recextlem1  8794  recexaplem2  8795  recexap  8796  crap0  9101  cju  9104  it0e0  9328  2mulicn  9329  iap0  9330  2muliap0  9331  cnref1o  9842  irec  10856  i2  10857  i3  10858  i4  10859  iexpcyc  10861  imval  11356  imre  11357  reim  11358  crre  11363  crim  11364  remim  11366  mulreap  11370  cjreb  11372  recj  11373  reneg  11374  readd  11375  remullem  11377  imcj  11381  imneg  11382  imadd  11383  cjadd  11390  cjneg  11396  imval2  11400  rei  11405  imi  11406  cji  11408  cjreim  11409  cjreim2  11410  cjap  11412  cnrecnv  11416  rennim  11508  absi  11565  absreimsq  11573  absreim  11574  absimle  11590  climcvg1nlem  11855  sinval  12208  cosval  12209  sinf  12210  cosf  12211  tanval2ap  12219  tanval3ap  12220  resinval  12221  recosval  12222  efi4p  12223  resin4p  12224  recos4p  12225  resincl  12226  recoscl  12227  sinneg  12232  cosneg  12233  efival  12238  efmival  12239  efeul  12240  sinadd  12242  cosadd  12243  ef01bndlem  12262  sin01bnd  12263  cos01bnd  12264  absef  12276  absefib  12277  efieq1re  12278  demoivre  12279  demoivreALT  12280  igz  12892  4sqlem17  12925  cnrehmeocntop  15278  sincn  15437  coscn  15438  efhalfpi  15467  ef2kpi  15474  efper  15475  sinperlem  15476  efimpi  15487  2sqlem2  15788  qdencn  16354