Theorem cnex 11148

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

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453  ℂcc 11065

This theorem was proved from axioms:  ax-cnex 11123

This theorem is referenced by:  reex  11158  cnelprrecn  11160  pnfex  11229  nnex  12210  zex  12571  qex  12956  mpoaddex  12983  addex  12984  mpomulex  12985  mulex  12986  rlim  15513  rlimf  15519  rlimss  15520  elo12  15545  o1f  15547  o1dm  15548  cnso  16270  cnaddablx  19899  cnaddabl  19900  cnaddid  19901  cnaddinv  19902  cnfldbas  21416  cnfldcj  21421  cnfldds  21424  cnfldfun  21426  cnfldfunALT  21427  cnmsubglem  21470  cnmsgngrp  21619  psgninv  21622  lmbrf  23308  lmfss  23344  lmres  23348  lmcnp  23352  cnmet  24819  cncfval  24938  elcncf  24939  cncfcnvcn  24975  cnheibor  25005  cnlmodlem1  25186  tcphex  25267  tchnmfval  25278  tcphcph  25287  lmmbr2  25309  lmmbrf  25312  iscau2  25327  iscauf  25330  caucfil  25333  cmetcaulem  25338  caussi  25347  causs  25348  lmclimf  25354  mbff  25675  ismbf  25678  ismbfcn  25679  mbfconst  25683  mbfres  25694  mbfimaopn2  25707  cncombf  25708  cnmbf  25709  0plef  25722  0pledm  25723  itg1ge0  25736  mbfi1fseqlem5  25769  itg2addlem  25808  limcfval  25922  limcrcl  25924  ellimc2  25927  limcflf  25931  limcres  25936  limcun  25945  dvfval  25947  dvbss  25951  dvbsss  25952  perfdvf  25953  dvreslem  25959  dvres2lem  25960  dvcnp2  25970  dvnfval  25972  dvnff  25973  dvnf  25977  dvnbss  25978  dvnadd  25979  dvn2bss  25980  dvnres  25981  cpnfval  25982  cpnord  25985  dvaddbr  25988  dvmulbr  25989  dvnfre  26002  dvexp  26003  dvef  26030  c1liplem1  26046  c1lip2  26048  lhop1lem  26063  plyval  26241  elply  26243  elply2  26244  plyf  26246  plyss  26247  elplyr  26249  plyeq0lem  26258  plyeq0  26259  plypf1  26260  plyaddlem1  26261  plymullem1  26262  plyaddlem  26263  plymullem  26264  plysub  26267  coeeulem  26272  coeeq  26275  dgrlem  26277  coeidlem  26285  plyco  26289  coe0  26304  coesub  26305  dgrmulc  26319  dgrsub  26320  dgrcolem1  26321  dgrcolem2  26322  plymul0or  26330  plymul02  26332  plyn0mulidp  26333  dvnply2  26339  plycpn  26341  plydivlem3  26347  plydivlem4  26348  plydiveu  26350  plyremlem  26356  plyrem  26357  facth  26358  fta1lem  26359  quotcan  26361  vieta1lem2  26363  plyexmo  26365  elqaalem3  26373  qaa  26375  iaa  26377  aannenlem1  26380  aannenlem2  26381  aannenlem3  26382  taylfvallem1  26408  taylfval  26410  tayl0  26413  taylplem1  26414  taylply2  26419  taylply  26420  dvtaylp  26421  dvntaylp  26422  dvntaylp0  26423  taylthlem1  26424  taylthlem2  26425  ulmval  26431  ulmss  26448  ulmcn  26450  mtest  26455  pserulm  26473  psercn  26477  pserdvlem2  26479  abelth  26492  reefgim  26501  cxpcn2  26799  logbmpt  26841  logbfval  26843  lgamgulmlem5  27085  lgamgulmlem6  27086  lgamgulm2  27088  lgamcvglem  27092  ftalem7  27131  dchrfi  27307  cffldtocusgr  29605  isvcOLD  30739  cnaddabloOLD  30741  cnnvg  30838  cnnvs  30840  cnnvnm  30841  cncph  30979  hvmulex  31171  hfsmval  31898  hfmmval  31899  nmfnval  32036  nlfnval  32041  elcnfn  32042  ellnfn  32043  specval  32058  hhcnf  32065  constrsuc  33996  lmlim  34205  esumcvg  34344  signsplypnf  34805  signsply0  34806  breprexplemb  34886  breprexpnat  34889  vtsval  34892  circlemethnat  34896  circlevma  34897  circlemethhgt  34898  cvxpconn  35553  fwddifval  36473  fwddifnval  36474  ivthALT  36656  knoppcnlem5  36896  knoppcnlem8  36899  bj-inftyexpiinv  37661  bj-inftyexpidisj  37663  caures  38220  cntotbnd  38256  cnpwstotbnd  38257  rrnval  38287  cnaddcom  39557  subex  42824  absex  42825  cjex  42826  elmnc  43674  mpaaeu  43688  itgoval  43699  itgocn  43702  rngunsnply  43707  binomcxplemnotnn0  44893  climexp  46142  xlimbr  46362  fuzxrpmcn  46363  xlimmnfvlem2  46368  xlimpnfvlem2  46372  mulcncff  46405  subcncff  46415  addcncff  46419  cncfuni  46421  divcncff  46426  dvsinax  46448  dvcosax  46461  dvnmptdivc  46473  dvnmptconst  46476  dvnxpaek  46477  dvnmul  46478  dvnprodlem3  46483  etransclem1  46770  etransclem2  46771  etransclem4  46773  etransclem13  46782  etransclem46  46815  nthrucw  47423  cjnpoly  47444  fdivpm  49126  amgmlemALT  50385