MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnex Structured version   Visualization version   GIF version

Theorem cnex 10607
Description: Alias for ax-cnex 10582. See also cnexALT 12373. (Contributed by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
cnex ℂ ∈ V

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 10582 1 ℂ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2111  Vcvv 3441  cc 10524
This theorem was proved from axioms:  ax-cnex 10582
This theorem is referenced by:  reex  10617  cnelprrecn  10619  pnfex  10683  nnex  11631  zex  11978  qex  12348  addex  12375  mulex  12376  rlim  14844  rlimf  14850  rlimss  14851  elo12  14876  o1f  14878  o1dm  14879  cnso  15592  cnaddablx  18981  cnaddabl  18982  cnaddid  18983  cnaddinv  18984  cnfldbas  20095  cnfldcj  20098  cnfldds  20101  cnfldfun  20103  cnfldfunALT  20104  cnmsubglem  20154  cnmsgngrp  20268  psgninv  20271  lmbrf  21865  lmfss  21901  lmres  21905  lmcnp  21909  cnmet  23377  cncfval  23493  elcncf  23494  cncfcnvcn  23530  cnheibor  23560  cnlmodlem1  23741  tcphex  23821  tchnmfval  23832  tcphcph  23841  lmmbr2  23863  lmmbrf  23866  iscau2  23881  iscauf  23884  caucfil  23887  cmetcaulem  23892  caussi  23901  causs  23902  lmclimf  23908  mbff  24229  ismbf  24232  ismbfcn  24233  mbfconst  24237  mbfres  24248  mbfimaopn2  24261  cncombf  24262  cnmbf  24263  0plef  24276  0pledm  24277  itg1ge0  24290  mbfi1fseqlem5  24323  itg2addlem  24362  limcfval  24475  limcrcl  24477  ellimc2  24480  limcflf  24484  limcres  24489  limcun  24498  dvfval  24500  dvbss  24504  dvbsss  24505  perfdvf  24506  dvreslem  24512  dvres2lem  24513  dvcnp2  24523  dvnfval  24525  dvnff  24526  dvnf  24530  dvnbss  24531  dvnadd  24532  dvn2bss  24533  dvnres  24534  cpnfval  24535  cpnord  24538  dvaddbr  24541  dvmulbr  24542  dvnfre  24555  dvexp  24556  dvef  24583  c1liplem1  24599  c1lip2  24601  lhop1lem  24616  plyval  24790  elply  24792  elply2  24793  plyf  24795  plyss  24796  elplyr  24798  plyeq0lem  24807  plyeq0  24808  plypf1  24809  plyaddlem1  24810  plymullem1  24811  plyaddlem  24812  plymullem  24813  plysub  24816  coeeulem  24821  coeeq  24824  dgrlem  24826  coeidlem  24834  plyco  24838  coe0  24853  coesub  24854  dgrmulc  24868  dgrsub  24869  dgrcolem1  24870  dgrcolem2  24871  plymul0or  24877  dvnply2  24883  plycpn  24885  plydivlem3  24891  plydivlem4  24892  plydiveu  24894  plyremlem  24900  plyrem  24901  facth  24902  fta1lem  24903  quotcan  24905  vieta1lem2  24907  plyexmo  24909  elqaalem3  24917  qaa  24919  iaa  24921  aannenlem1  24924  aannenlem2  24925  aannenlem3  24926  taylfvallem1  24952  taylfval  24954  tayl0  24957  taylplem1  24958  taylply2  24963  taylply  24964  dvtaylp  24965  dvntaylp  24966  dvntaylp0  24967  taylthlem1  24968  taylthlem2  24969  ulmval  24975  ulmss  24992  ulmcn  24994  mtest  24999  pserulm  25017  psercn  25021  pserdvlem2  25023  abelth  25036  reefgim  25045  cxpcn2  25335  logbmpt  25374  logbfval  25376  lgamgulmlem5  25618  lgamgulmlem6  25619  lgamgulm2  25621  lgamcvglem  25625  ftalem7  25664  dchrfi  25839  cffldtocusgr  27237  isvcOLD  28362  cnaddabloOLD  28364  cnnvg  28461  cnnvs  28463  cnnvnm  28464  cncph  28602  hvmulex  28794  hfsmval  29521  hfmmval  29522  nmfnval  29659  nlfnval  29664  elcnfn  29665  ellnfn  29666  specval  29681  hhcnf  29688  lmlim  31300  esumcvg  31455  plymul02  31926  plymulx0  31927  signsplypnf  31930  signsply0  31931  breprexplemb  32012  breprexpnat  32015  vtsval  32018  circlemethnat  32022  circlevma  32023  circlemethhgt  32024  cvxpconn  32602  fwddifval  33736  fwddifnval  33737  ivthALT  33796  knoppcnlem5  33949  knoppcnlem8  33952  bj-inftyexpiinv  34623  bj-inftyexpidisj  34625  caures  35198  cntotbnd  35234  cnpwstotbnd  35235  rrnval  35265  cnaddcom  36268  elmnc  40080  mpaaeu  40094  itgoval  40105  itgocn  40108  rngunsnply  40117  binomcxplemnotnn0  41060  climexp  42247  xlimbr  42469  fuzxrpmcn  42470  xlimmnfvlem2  42475  xlimpnfvlem2  42479  mulcncff  42512  subcncff  42522  addcncff  42526  cncfuni  42528  divcncff  42533  dvsinax  42555  dvcosax  42568  dvnmptdivc  42580  dvnmptconst  42583  dvnxpaek  42584  dvnmul  42585  dvnprodlem3  42590  etransclem1  42877  etransclem2  42878  etransclem4  42880  etransclem13  42889  etransclem46  42922  fdivpm  44957  amgmlemALT  45331
  Copyright terms: Public domain W3C validator