Theorem cnex 10017

Description: Alias for ax-cnex 9992. See also cnexALT 11828. (Contributed by Mario Carneiro, 17-Nov-2014.)

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

Step	Hyp	Ref	Expression
1		ax-cnex 9992	1 ⊢ ℂ ∈ V

Syntax hints:   ∈ wcel 1990  Vcvv 3200  ℂcc 9934

This theorem was proved from axioms:  ax-cnex 9992

This theorem is referenced by:  reex  10027  cnelprrecn  10029  pnfxr  10092  nnex  11026  zex  11386  qex  11800  addex  11830  mulex  11831  rlim  14226  rlimf  14232  rlimss  14233  elo12  14258  o1f  14260  o1dm  14261  cnso  14976  cnaddablx  18271  cnaddabl  18272  cnaddid  18273  cnaddinv  18274  cnfldbas  19750  cnfldcj  19753  cnfldds  19756  cnfldfun  19758  cnfldfunALT  19759  cnmsubglem  19809  cnmsgngrp  19925  psgninv  19928  lmbrf  21064  lmfss  21100  lmres  21104  lmcnp  21108  cnmet  22575  cncfval  22691  elcncf  22692  cncfcnvcn  22724  cnheibor  22754  cnlmodlem1  22936  tchex  23016  tchnmfval  23027  tchcph  23036  lmmbr2  23057  lmmbrf  23060  iscau2  23075  iscauf  23078  caucfil  23081  cmetcaulem  23086  caussi  23095  causs  23096  lmclimf  23102  mbff  23394  ismbf  23397  ismbfcn  23398  mbfconst  23402  mbfres  23411  mbfimaopn2  23424  cncombf  23425  cnmbf  23426  0plef  23439  0pledm  23440  itg1ge0  23453  mbfi1fseqlem5  23486  itg2addlem  23525  limcfval  23636  limcrcl  23638  ellimc2  23641  limcflf  23645  limcres  23650  limcun  23659  dvfval  23661  dvbss  23665  dvbsss  23666  perfdvf  23667  dvreslem  23673  dvres2lem  23674  dvcnp2  23683  dvnfval  23685  dvnff  23686  dvnf  23690  dvnbss  23691  dvnadd  23692  dvn2bss  23693  dvnres  23694  cpnfval  23695  cpnord  23698  dvaddbr  23701  dvmulbr  23702  dvnfre  23715  dvexp  23716  dvef  23743  c1liplem1  23759  c1lip2  23761  lhop1lem  23776  plyval  23949  elply  23951  elply2  23952  plyf  23954  plyss  23955  elplyr  23957  plyeq0lem  23966  plyeq0  23967  plypf1  23968  plyaddlem1  23969  plymullem1  23970  plyaddlem  23971  plymullem  23972  plysub  23975  coeeulem  23980  coeeq  23983  dgrlem  23985  coeidlem  23993  plyco  23997  coe0  24012  coesub  24013  dgrmulc  24027  dgrsub  24028  dgrcolem1  24029  dgrcolem2  24030  plymul0or  24036  dvnply2  24042  plycpn  24044  plydivlem3  24050  plydivlem4  24051  plydiveu  24053  plyremlem  24059  plyrem  24060  facth  24061  fta1lem  24062  quotcan  24064  vieta1lem2  24066  plyexmo  24068  elqaalem3  24076  qaa  24078  iaa  24080  aannenlem1  24083  aannenlem2  24084  aannenlem3  24085  taylfvallem1  24111  taylfval  24113  tayl0  24116  taylplem1  24117  taylply2  24122  taylply  24123  dvtaylp  24124  dvntaylp  24125  dvntaylp0  24126  taylthlem1  24127  taylthlem2  24128  ulmval  24134  ulmss  24151  ulmcn  24153  mtest  24158  pserulm  24176  psercn  24180  pserdvlem2  24182  abelth  24195  reefgim  24204  cxpcn2  24487  logbmpt  24526  logbfval  24528  lgamgulmlem5  24759  lgamgulmlem6  24760  lgamgulm2  24762  lgamcvglem  24766  ftalem7  24805  dchrfi  24980  cffldtocusgr  26343  isvcOLD  27434  cnaddabloOLD  27436  cnnvg  27533  cnnvs  27535  cnnvnm  27536  cncph  27674  hvmulex  27868  hfsmval  28597  hfmmval  28598  nmfnval  28735  nlfnval  28740  elcnfn  28741  ellnfn  28742  specval  28757  hhcnf  28764  lmlim  29993  esumcvg  30148  plymul02  30623  plymulx0  30624  signsplypnf  30627  signsply0  30628  breprexplemb  30709  breprexpnat  30712  vtsval  30715  circlemethnat  30719  circlevma  30720  circlemethhgt  30721  cvxpconn  31224  fwddifval  32269  fwddifnval  32270  ivthALT  32330  knoppcnlem5  32487  knoppcnlem8  32490  bj-inftyexpiinv  33095  bj-inftyexpidisj  33097  caures  33556  cntotbnd  33595  cnpwstotbnd  33596  rrnval  33626  cnaddcom  34259  elmnc  37706  mpaaeu  37720  itgoval  37731  itgocn  37734  rngunsnply  37743  binomcxplemnotnn0  38555  climexp  39837  xlimbr  40053  fuzxrpmcn  40054  xlimmnfvlem2  40059  xlimpnfvlem2  40063  mulcncff  40081  subcncff  40093  addcncff  40097  cncfuni  40099  divcncff  40104  dvsinax  40127  dvcosax  40141  dvnmptdivc  40153  dvnmptconst  40156  dvnxpaek  40157  dvnmul  40158  dvnprodlem3  40163  etransclem1  40452  etransclem2  40453  etransclem4  40455  etransclem13  40464  etransclem46  40497  fdivpm  42337  amgmlemALT  42549