Theorem cnex 11156

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

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450  ℂcc 11073

This theorem was proved from axioms:  ax-cnex 11131

This theorem is referenced by:  reex  11166  cnelprrecn  11168  pnfex  11234  nnex  12199  zex  12545  qex  12927  mpoaddex  12954  addex  12955  mpomulex  12956  mulex  12957  rlim  15468  rlimf  15474  rlimss  15475  elo12  15500  o1f  15502  o1dm  15503  cnso  16222  cnaddablx  19805  cnaddabl  19806  cnaddid  19807  cnaddinv  19808  cnfldbas  21275  cnfldcj  21280  cnfldds  21283  cnfldfun  21285  cnfldfunALT  21286  cnfldbasOLD  21290  cnfldcjOLD  21293  cnflddsOLD  21296  cnfldfunOLD  21298  cnfldfunALTOLD  21299  cnmsubglem  21354  cnmsgngrp  21495  psgninv  21498  lmbrf  23154  lmfss  23190  lmres  23194  lmcnp  23198  cnmet  24666  cncfval  24788  elcncf  24789  cncfcnvcn  24826  cnheibor  24861  cnlmodlem1  25043  tcphex  25124  tchnmfval  25135  tcphcph  25144  lmmbr2  25166  lmmbrf  25169  iscau2  25184  iscauf  25187  caucfil  25190  cmetcaulem  25195  caussi  25204  causs  25205  lmclimf  25211  mbff  25533  ismbf  25536  ismbfcn  25537  mbfconst  25541  mbfres  25552  mbfimaopn2  25565  cncombf  25566  cnmbf  25567  0plef  25580  0pledm  25581  itg1ge0  25594  mbfi1fseqlem5  25627  itg2addlem  25666  limcfval  25780  limcrcl  25782  ellimc2  25785  limcflf  25789  limcres  25794  limcun  25803  dvfval  25805  dvbss  25809  dvbsss  25810  perfdvf  25811  dvreslem  25817  dvres2lem  25818  dvcnp2  25828  dvcnp2OLD  25829  dvnfval  25831  dvnff  25832  dvnf  25836  dvnbss  25837  dvnadd  25838  dvn2bss  25839  dvnres  25840  cpnfval  25841  cpnord  25844  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvnfre  25863  dvexp  25864  dvef  25891  c1liplem1  25908  c1lip2  25910  lhop1lem  25925  plyval  26105  elply  26107  elply2  26108  plyf  26110  plyss  26111  elplyr  26113  plyeq0lem  26122  plyeq0  26123  plypf1  26124  plyaddlem1  26125  plymullem1  26126  plyaddlem  26127  plymullem  26128  plysub  26131  coeeulem  26136  coeeq  26139  dgrlem  26141  coeidlem  26149  plyco  26153  coe0  26168  coesub  26169  dgrmulc  26184  dgrsub  26185  dgrcolem1  26186  dgrcolem2  26187  plymul0or  26195  dvnply2  26202  plycpn  26204  plydivlem3  26210  plydivlem4  26211  plydiveu  26213  plyremlem  26219  plyrem  26220  facth  26221  fta1lem  26222  quotcan  26224  vieta1lem2  26226  plyexmo  26228  elqaalem3  26236  qaa  26238  iaa  26240  aannenlem1  26243  aannenlem2  26244  aannenlem3  26245  taylfvallem1  26271  taylfval  26273  tayl0  26276  taylplem1  26277  taylply2  26282  taylply2OLD  26283  taylply  26284  dvtaylp  26285  dvntaylp  26286  dvntaylp0  26287  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  ulmval  26296  ulmss  26313  ulmcn  26315  mtest  26320  pserulm  26338  psercn  26343  pserdvlem2  26345  abelth  26358  reefgim  26367  cxpcn2  26663  logbmpt  26705  logbfval  26707  lgamgulmlem5  26950  lgamgulmlem6  26951  lgamgulm2  26953  lgamcvglem  26957  ftalem7  26996  dchrfi  27173  cffldtocusgr  29381  cffldtocusgrOLD  29382  isvcOLD  30515  cnaddabloOLD  30517  cnnvg  30614  cnnvs  30616  cnnvnm  30617  cncph  30755  hvmulex  30947  hfsmval  31674  hfmmval  31675  nmfnval  31812  nlfnval  31817  elcnfn  31818  ellnfn  31819  specval  31834  hhcnf  31841  constrsuc  33735  lmlim  33944  esumcvg  34083  plymul02  34544  plymulx0  34545  signsplypnf  34548  signsply0  34549  breprexplemb  34629  breprexpnat  34632  vtsval  34635  circlemethnat  34639  circlevma  34640  circlemethhgt  34641  cvxpconn  35236  fwddifval  36157  fwddifnval  36158  ivthALT  36330  knoppcnlem5  36492  knoppcnlem8  36495  bj-inftyexpiinv  37203  bj-inftyexpidisj  37205  caures  37761  cntotbnd  37797  cnpwstotbnd  37798  rrnval  37828  cnaddcom  38972  subex  42242  absex  42243  cjex  42244  elmnc  43132  mpaaeu  43146  itgoval  43157  itgocn  43160  rngunsnply  43165  binomcxplemnotnn0  44352  climexp  45610  xlimbr  45832  fuzxrpmcn  45833  xlimmnfvlem2  45838  xlimpnfvlem2  45842  mulcncff  45875  subcncff  45885  addcncff  45889  cncfuni  45891  divcncff  45896  dvsinax  45918  dvcosax  45931  dvnmptdivc  45943  dvnmptconst  45946  dvnxpaek  45947  dvnmul  45948  dvnprodlem3  45953  etransclem1  46240  etransclem2  46241  etransclem4  46243  etransclem13  46252  etransclem46  46285  fdivpm  48536  amgmlemALT  49796