Theorem cnex 10055

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

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

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

Syntax hints:   ∈ wcel 2030  Vcvv 3231  ℂcc 9972

This theorem was proved from axioms:  ax-cnex 10030

This theorem is referenced by:  reex  10065  cnelprrecn  10067  pnfxr  10130  nnex  11064  zex  11424  qex  11838  addex  11868  mulex  11869  rlim  14270  rlimf  14276  rlimss  14277  elo12  14302  o1f  14304  o1dm  14305  cnso  15020  cnaddablx  18317  cnaddabl  18318  cnaddid  18319  cnaddinv  18320  cnfldbas  19798  cnfldcj  19801  cnfldds  19804  cnfldfun  19806  cnfldfunALT  19807  cnmsubglem  19857  cnmsgngrp  19973  psgninv  19976  lmbrf  21112  lmfss  21148  lmres  21152  lmcnp  21156  cnmet  22622  cncfval  22738  elcncf  22739  cncfcnvcn  22771  cnheibor  22801  cnlmodlem1  22982  tchex  23062  tchnmfval  23073  tchcph  23082  lmmbr2  23103  lmmbrf  23106  iscau2  23121  iscauf  23124  caucfil  23127  cmetcaulem  23132  caussi  23141  causs  23142  lmclimf  23148  mbff  23439  ismbf  23442  ismbfcn  23443  mbfconst  23447  mbfres  23456  mbfimaopn2  23469  cncombf  23470  cnmbf  23471  0plef  23484  0pledm  23485  itg1ge0  23498  mbfi1fseqlem5  23531  itg2addlem  23570  limcfval  23681  limcrcl  23683  ellimc2  23686  limcflf  23690  limcres  23695  limcun  23704  dvfval  23706  dvbss  23710  dvbsss  23711  perfdvf  23712  dvreslem  23718  dvres2lem  23719  dvcnp2  23728  dvnfval  23730  dvnff  23731  dvnf  23735  dvnbss  23736  dvnadd  23737  dvn2bss  23738  dvnres  23739  cpnfval  23740  cpnord  23743  dvaddbr  23746  dvmulbr  23747  dvnfre  23760  dvexp  23761  dvef  23788  c1liplem1  23804  c1lip2  23806  lhop1lem  23821  plyval  23994  elply  23996  elply2  23997  plyf  23999  plyss  24000  elplyr  24002  plyeq0lem  24011  plyeq0  24012  plypf1  24013  plyaddlem1  24014  plymullem1  24015  plyaddlem  24016  plymullem  24017  plysub  24020  coeeulem  24025  coeeq  24028  dgrlem  24030  coeidlem  24038  plyco  24042  coe0  24057  coesub  24058  dgrmulc  24072  dgrsub  24073  dgrcolem1  24074  dgrcolem2  24075  plymul0or  24081  dvnply2  24087  plycpn  24089  plydivlem3  24095  plydivlem4  24096  plydiveu  24098  plyremlem  24104  plyrem  24105  facth  24106  fta1lem  24107  quotcan  24109  vieta1lem2  24111  plyexmo  24113  elqaalem3  24121  qaa  24123  iaa  24125  aannenlem1  24128  aannenlem2  24129  aannenlem3  24130  taylfvallem1  24156  taylfval  24158  tayl0  24161  taylplem1  24162  taylply2  24167  taylply  24168  dvtaylp  24169  dvntaylp  24170  dvntaylp0  24171  taylthlem1  24172  taylthlem2  24173  ulmval  24179  ulmss  24196  ulmcn  24198  mtest  24203  pserulm  24221  psercn  24225  pserdvlem2  24227  abelth  24240  reefgim  24249  cxpcn2  24532  logbmpt  24571  logbfval  24573  lgamgulmlem5  24804  lgamgulmlem6  24805  lgamgulm2  24807  lgamcvglem  24811  ftalem7  24850  dchrfi  25025  cffldtocusgr  26399  isvcOLD  27562  cnaddabloOLD  27564  cnnvg  27661  cnnvs  27663  cnnvnm  27664  cncph  27802  hvmulex  27996  hfsmval  28725  hfmmval  28726  nmfnval  28863  nlfnval  28868  elcnfn  28869  ellnfn  28870  specval  28885  hhcnf  28892  lmlim  30121  esumcvg  30276  plymul02  30751  plymulx0  30752  signsplypnf  30755  signsply0  30756  breprexplemb  30837  breprexpnat  30840  vtsval  30843  circlemethnat  30847  circlevma  30848  circlemethhgt  30849  cvxpconn  31350  fwddifval  32394  fwddifnval  32395  ivthALT  32455  knoppcnlem5  32612  knoppcnlem8  32615  bj-inftyexpiinv  33225  bj-inftyexpidisj  33227  caures  33686  cntotbnd  33725  cnpwstotbnd  33726  rrnval  33756  cnaddcom  34577  elmnc  38023  mpaaeu  38037  itgoval  38048  itgocn  38051  rngunsnply  38060  binomcxplemnotnn0  38872  climexp  40155  xlimbr  40371  fuzxrpmcn  40372  xlimmnfvlem2  40377  xlimpnfvlem2  40381  mulcncff  40399  subcncff  40411  addcncff  40415  cncfuni  40417  divcncff  40422  dvsinax  40445  dvcosax  40459  dvnmptdivc  40471  dvnmptconst  40474  dvnxpaek  40475  dvnmul  40476  dvnprodlem3  40481  etransclem1  40770  etransclem2  40771  etransclem4  40773  etransclem13  40782  etransclem46  40815  fdivpm  42662  amgmlemALT  42877