Theorem cnex 10883

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

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422  ℂcc 10800

This theorem was proved from axioms:  ax-cnex 10858

This theorem is referenced by:  reex  10893  cnelprrecn  10895  pnfex  10959  nnex  11909  zex  12258  qex  12630  addex  12657  mulex  12658  rlim  15132  rlimf  15138  rlimss  15139  elo12  15164  o1f  15166  o1dm  15167  cnso  15884  cnaddablx  19384  cnaddabl  19385  cnaddid  19386  cnaddinv  19387  cnfldbas  20514  cnfldcj  20517  cnfldds  20520  cnfldfun  20522  cnfldfunALT  20523  cnmsubglem  20573  cnmsgngrp  20696  psgninv  20699  lmbrf  22319  lmfss  22355  lmres  22359  lmcnp  22363  cnmet  23841  cncfval  23957  elcncf  23958  cncfcnvcn  23994  cnheibor  24024  cnlmodlem1  24205  tcphex  24286  tchnmfval  24297  tcphcph  24306  lmmbr2  24328  lmmbrf  24331  iscau2  24346  iscauf  24349  caucfil  24352  cmetcaulem  24357  caussi  24366  causs  24367  lmclimf  24373  mbff  24694  ismbf  24697  ismbfcn  24698  mbfconst  24702  mbfres  24713  mbfimaopn2  24726  cncombf  24727  cnmbf  24728  0plef  24741  0pledm  24742  itg1ge0  24755  mbfi1fseqlem5  24789  itg2addlem  24828  limcfval  24941  limcrcl  24943  ellimc2  24946  limcflf  24950  limcres  24955  limcun  24964  dvfval  24966  dvbss  24970  dvbsss  24971  perfdvf  24972  dvreslem  24978  dvres2lem  24979  dvcnp2  24989  dvnfval  24991  dvnff  24992  dvnf  24996  dvnbss  24997  dvnadd  24998  dvn2bss  24999  dvnres  25000  cpnfval  25001  cpnord  25004  dvaddbr  25007  dvmulbr  25008  dvnfre  25021  dvexp  25022  dvef  25049  c1liplem1  25065  c1lip2  25067  lhop1lem  25082  plyval  25259  elply  25261  elply2  25262  plyf  25264  plyss  25265  elplyr  25267  plyeq0lem  25276  plyeq0  25277  plypf1  25278  plyaddlem1  25279  plymullem1  25280  plyaddlem  25281  plymullem  25282  plysub  25285  coeeulem  25290  coeeq  25293  dgrlem  25295  coeidlem  25303  plyco  25307  coe0  25322  coesub  25323  dgrmulc  25337  dgrsub  25338  dgrcolem1  25339  dgrcolem2  25340  plymul0or  25346  dvnply2  25352  plycpn  25354  plydivlem3  25360  plydivlem4  25361  plydiveu  25363  plyremlem  25369  plyrem  25370  facth  25371  fta1lem  25372  quotcan  25374  vieta1lem2  25376  plyexmo  25378  elqaalem3  25386  qaa  25388  iaa  25390  aannenlem1  25393  aannenlem2  25394  aannenlem3  25395  taylfvallem1  25421  taylfval  25423  tayl0  25426  taylplem1  25427  taylply2  25432  taylply  25433  dvtaylp  25434  dvntaylp  25435  dvntaylp0  25436  taylthlem1  25437  taylthlem2  25438  ulmval  25444  ulmss  25461  ulmcn  25463  mtest  25468  pserulm  25486  psercn  25490  pserdvlem2  25492  abelth  25505  reefgim  25514  cxpcn2  25804  logbmpt  25843  logbfval  25845  lgamgulmlem5  26087  lgamgulmlem6  26088  lgamgulm2  26090  lgamcvglem  26094  ftalem7  26133  dchrfi  26308  cffldtocusgr  27717  isvcOLD  28842  cnaddabloOLD  28844  cnnvg  28941  cnnvs  28943  cnnvnm  28944  cncph  29082  hvmulex  29274  hfsmval  30001  hfmmval  30002  nmfnval  30139  nlfnval  30144  elcnfn  30145  ellnfn  30146  specval  30161  hhcnf  30168  lmlim  31799  esumcvg  31954  plymul02  32425  plymulx0  32426  signsplypnf  32429  signsply0  32430  breprexplemb  32511  breprexpnat  32514  vtsval  32517  circlemethnat  32521  circlevma  32522  circlemethhgt  32523  cvxpconn  33104  fwddifval  34391  fwddifnval  34392  ivthALT  34451  knoppcnlem5  34604  knoppcnlem8  34607  bj-inftyexpiinv  35306  bj-inftyexpidisj  35308  caures  35845  cntotbnd  35881  cnpwstotbnd  35882  rrnval  35912  cnaddcom  36913  elmnc  40877  mpaaeu  40891  itgoval  40902  itgocn  40905  rngunsnply  40914  binomcxplemnotnn0  41863  climexp  43036  xlimbr  43258  fuzxrpmcn  43259  xlimmnfvlem2  43264  xlimpnfvlem2  43268  mulcncff  43301  subcncff  43311  addcncff  43315  cncfuni  43317  divcncff  43322  dvsinax  43344  dvcosax  43357  dvnmptdivc  43369  dvnmptconst  43372  dvnxpaek  43373  dvnmul  43374  dvnprodlem3  43379  etransclem1  43666  etransclem2  43667  etransclem4  43669  etransclem13  43678  etransclem46  43711  fdivpm  45777  amgmlemALT  46393