Theorem cnex 11236

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

Assertion

Ref	Expression
cnex	⊢ ℂ ∈ V

Proof of Theorem cnex

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480  ℂcc 11153

This theorem was proved from axioms:  ax-cnex 11211

This theorem is referenced by:  reex  11246  cnelprrecn  11248  pnfex  11314  nnex  12272  zex  12622  qex  13003  mpoaddex  13030  addex  13031  mpomulex  13032  mulex  13033  rlim  15531  rlimf  15537  rlimss  15538  elo12  15563  o1f  15565  o1dm  15566  cnso  16283  cnaddablx  19886  cnaddabl  19887  cnaddid  19888  cnaddinv  19889  cnfldbas  21368  cnfldcj  21373  cnfldds  21376  cnfldfun  21378  cnfldfunALT  21379  cnfldbasOLD  21383  cnfldcjOLD  21386  cnflddsOLD  21389  cnfldfunOLD  21391  cnfldfunALTOLD  21392  cnfldfunALTOLDOLD  21393  cnmsubglem  21448  cnmsgngrp  21597  psgninv  21600  lmbrf  23268  lmfss  23304  lmres  23308  lmcnp  23312  cnmet  24792  cncfval  24914  elcncf  24915  cncfcnvcn  24952  cnheibor  24987  cnlmodlem1  25169  tcphex  25251  tchnmfval  25262  tcphcph  25271  lmmbr2  25293  lmmbrf  25296  iscau2  25311  iscauf  25314  caucfil  25317  cmetcaulem  25322  caussi  25331  causs  25332  lmclimf  25338  mbff  25660  ismbf  25663  ismbfcn  25664  mbfconst  25668  mbfres  25679  mbfimaopn2  25692  cncombf  25693  cnmbf  25694  0plef  25707  0pledm  25708  itg1ge0  25721  mbfi1fseqlem5  25754  itg2addlem  25793  limcfval  25907  limcrcl  25909  ellimc2  25912  limcflf  25916  limcres  25921  limcun  25930  dvfval  25932  dvbss  25936  dvbsss  25937  perfdvf  25938  dvreslem  25944  dvres2lem  25945  dvcnp2  25955  dvcnp2OLD  25956  dvnfval  25958  dvnff  25959  dvnf  25963  dvnbss  25964  dvnadd  25965  dvn2bss  25966  dvnres  25967  cpnfval  25968  cpnord  25971  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvnfre  25990  dvexp  25991  dvef  26018  c1liplem1  26035  c1lip2  26037  lhop1lem  26052  plyval  26232  elply  26234  elply2  26235  plyf  26237  plyss  26238  elplyr  26240  plyeq0lem  26249  plyeq0  26250  plypf1  26251  plyaddlem1  26252  plymullem1  26253  plyaddlem  26254  plymullem  26255  plysub  26258  coeeulem  26263  coeeq  26266  dgrlem  26268  coeidlem  26276  plyco  26280  coe0  26295  coesub  26296  dgrmulc  26311  dgrsub  26312  dgrcolem1  26313  dgrcolem2  26314  plymul0or  26322  dvnply2  26329  plycpn  26331  plydivlem3  26337  plydivlem4  26338  plydiveu  26340  plyremlem  26346  plyrem  26347  facth  26348  fta1lem  26349  quotcan  26351  vieta1lem2  26353  plyexmo  26355  elqaalem3  26363  qaa  26365  iaa  26367  aannenlem1  26370  aannenlem2  26371  aannenlem3  26372  taylfvallem1  26398  taylfval  26400  tayl0  26403  taylplem1  26404  taylply2  26409  taylply2OLD  26410  taylply  26411  dvtaylp  26412  dvntaylp  26413  dvntaylp0  26414  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmval  26423  ulmss  26440  ulmcn  26442  mtest  26447  pserulm  26465  psercn  26470  pserdvlem2  26472  abelth  26485  reefgim  26494  cxpcn2  26789  logbmpt  26831  logbfval  26833  lgamgulmlem5  27076  lgamgulmlem6  27077  lgamgulm2  27079  lgamcvglem  27083  ftalem7  27122  dchrfi  27299  cffldtocusgr  29464  cffldtocusgrOLD  29465  isvcOLD  30598  cnaddabloOLD  30600  cnnvg  30697  cnnvs  30699  cnnvnm  30700  cncph  30838  hvmulex  31030  hfsmval  31757  hfmmval  31758  nmfnval  31895  nlfnval  31900  elcnfn  31901  ellnfn  31902  specval  31917  hhcnf  31924  constrsuc  33779  lmlim  33946  esumcvg  34087  plymul02  34561  plymulx0  34562  signsplypnf  34565  signsply0  34566  breprexplemb  34646  breprexpnat  34649  vtsval  34652  circlemethnat  34656  circlevma  34657  circlemethhgt  34658  cvxpconn  35247  fwddifval  36163  fwddifnval  36164  ivthALT  36336  knoppcnlem5  36498  knoppcnlem8  36501  bj-inftyexpiinv  37209  bj-inftyexpidisj  37211  caures  37767  cntotbnd  37803  cnpwstotbnd  37804  rrnval  37834  cnaddcom  38973  subex  42288  absex  42289  cjex  42290  elmnc  43148  mpaaeu  43162  itgoval  43173  itgocn  43176  rngunsnply  43181  binomcxplemnotnn0  44375  climexp  45620  xlimbr  45842  fuzxrpmcn  45843  xlimmnfvlem2  45848  xlimpnfvlem2  45852  mulcncff  45885  subcncff  45895  addcncff  45899  cncfuni  45901  divcncff  45906  dvsinax  45928  dvcosax  45941  dvnmptdivc  45953  dvnmptconst  45956  dvnxpaek  45957  dvnmul  45958  dvnprodlem3  45963  etransclem1  46250  etransclem2  46251  etransclem4  46253  etransclem13  46262  etransclem46  46295  fdivpm  48464  amgmlemALT  49322