Theorem cnex 11233

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

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

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

Syntax hints:   ∈ wcel 2105  Vcvv 3477  ℂcc 11150

This theorem was proved from axioms:  ax-cnex 11208

This theorem is referenced by:  reex  11243  cnelprrecn  11245  pnfex  11311  nnex  12269  zex  12619  qex  13000  mpoaddex  13027  addex  13028  mpomulex  13029  mulex  13030  rlim  15527  rlimf  15533  rlimss  15534  elo12  15559  o1f  15561  o1dm  15562  cnso  16279  cnaddablx  19900  cnaddabl  19901  cnaddid  19902  cnaddinv  19903  cnfldbas  21385  cnfldcj  21390  cnfldds  21393  cnfldfun  21395  cnfldfunALT  21396  cnfldbasOLD  21400  cnfldcjOLD  21403  cnflddsOLD  21406  cnfldfunOLD  21408  cnfldfunALTOLD  21409  cnfldfunALTOLDOLD  21410  cnmsubglem  21465  cnmsgngrp  21614  psgninv  21617  lmbrf  23283  lmfss  23319  lmres  23323  lmcnp  23327  cnmet  24807  cncfval  24927  elcncf  24928  cncfcnvcn  24965  cnheibor  25000  cnlmodlem1  25182  tcphex  25264  tchnmfval  25275  tcphcph  25284  lmmbr2  25306  lmmbrf  25309  iscau2  25324  iscauf  25327  caucfil  25330  cmetcaulem  25335  caussi  25344  causs  25345  lmclimf  25351  mbff  25673  ismbf  25676  ismbfcn  25677  mbfconst  25681  mbfres  25692  mbfimaopn2  25705  cncombf  25706  cnmbf  25707  0plef  25720  0pledm  25721  itg1ge0  25734  mbfi1fseqlem5  25768  itg2addlem  25807  limcfval  25921  limcrcl  25923  ellimc2  25926  limcflf  25930  limcres  25935  limcun  25944  dvfval  25946  dvbss  25950  dvbsss  25951  perfdvf  25952  dvreslem  25958  dvres2lem  25959  dvcnp2  25969  dvcnp2OLD  25970  dvnfval  25972  dvnff  25973  dvnf  25977  dvnbss  25978  dvnadd  25979  dvn2bss  25980  dvnres  25981  cpnfval  25982  cpnord  25985  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvnfre  26004  dvexp  26005  dvef  26032  c1liplem1  26049  c1lip2  26051  lhop1lem  26066  plyval  26246  elply  26248  elply2  26249  plyf  26251  plyss  26252  elplyr  26254  plyeq0lem  26263  plyeq0  26264  plypf1  26265  plyaddlem1  26266  plymullem1  26267  plyaddlem  26268  plymullem  26269  plysub  26272  coeeulem  26277  coeeq  26280  dgrlem  26282  coeidlem  26290  plyco  26294  coe0  26309  coesub  26310  dgrmulc  26325  dgrsub  26326  dgrcolem1  26327  dgrcolem2  26328  plymul0or  26336  dvnply2  26343  plycpn  26345  plydivlem3  26351  plydivlem4  26352  plydiveu  26354  plyremlem  26360  plyrem  26361  facth  26362  fta1lem  26363  quotcan  26365  vieta1lem2  26367  plyexmo  26369  elqaalem3  26377  qaa  26379  iaa  26381  aannenlem1  26384  aannenlem2  26385  aannenlem3  26386  taylfvallem1  26412  taylfval  26414  tayl0  26417  taylplem1  26418  taylply2  26423  taylply2OLD  26424  taylply  26425  dvtaylp  26426  dvntaylp  26427  dvntaylp0  26428  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmval  26437  ulmss  26454  ulmcn  26456  mtest  26461  pserulm  26479  psercn  26484  pserdvlem2  26486  abelth  26499  reefgim  26508  cxpcn2  26803  logbmpt  26845  logbfval  26847  lgamgulmlem5  27090  lgamgulmlem6  27091  lgamgulm2  27093  lgamcvglem  27097  ftalem7  27136  dchrfi  27313  cffldtocusgr  29478  cffldtocusgrOLD  29479  isvcOLD  30607  cnaddabloOLD  30609  cnnvg  30706  cnnvs  30708  cnnvnm  30709  cncph  30847  hvmulex  31039  hfsmval  31766  hfmmval  31767  nmfnval  31904  nlfnval  31909  elcnfn  31910  ellnfn  31911  specval  31926  hhcnf  31933  constrsuc  33742  lmlim  33907  esumcvg  34066  plymul02  34539  plymulx0  34540  signsplypnf  34543  signsply0  34544  breprexplemb  34624  breprexpnat  34627  vtsval  34630  circlemethnat  34634  circlevma  34635  circlemethhgt  34636  cvxpconn  35226  fwddifval  36143  fwddifnval  36144  ivthALT  36317  knoppcnlem5  36479  knoppcnlem8  36482  bj-inftyexpiinv  37190  bj-inftyexpidisj  37192  caures  37746  cntotbnd  37782  cnpwstotbnd  37783  rrnval  37813  cnaddcom  38953  subex  42266  absex  42267  cjex  42268  elmnc  43124  mpaaeu  43138  itgoval  43149  itgocn  43152  rngunsnply  43157  binomcxplemnotnn0  44351  climexp  45560  xlimbr  45782  fuzxrpmcn  45783  xlimmnfvlem2  45788  xlimpnfvlem2  45792  mulcncff  45825  subcncff  45835  addcncff  45839  cncfuni  45841  divcncff  45846  dvsinax  45868  dvcosax  45881  dvnmptdivc  45893  dvnmptconst  45896  dvnxpaek  45897  dvnmul  45898  dvnprodlem3  45903  etransclem1  46190  etransclem2  46191  etransclem4  46193  etransclem13  46202  etransclem46  46235  fdivpm  48392  amgmlemALT  49033