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 2114  Vcvv 3469  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  14843  rlimf  14849  rlimss  14850  elo12  14875  o1f  14877  o1dm  14878  cnso  15591  cnaddablx  18979  cnaddabl  18980  cnaddid  18981  cnaddinv  18982  cnfldbas  20093  cnfldcj  20096  cnfldds  20099  cnfldfun  20101  cnfldfunALT  20102  cnmsubglem  20152  cnmsgngrp  20266  psgninv  20269  lmbrf  21863  lmfss  21899  lmres  21903  lmcnp  21907  cnmet  23375  cncfval  23491  elcncf  23492  cncfcnvcn  23528  cnheibor  23558  cnlmodlem1  23739  tcphex  23819  tchnmfval  23830  tcphcph  23839  lmmbr2  23861  lmmbrf  23864  iscau2  23879  iscauf  23882  caucfil  23885  cmetcaulem  23890  caussi  23899  causs  23900  lmclimf  23906  mbff  24227  ismbf  24230  ismbfcn  24231  mbfconst  24235  mbfres  24246  mbfimaopn2  24259  cncombf  24260  cnmbf  24261  0plef  24274  0pledm  24275  itg1ge0  24288  mbfi1fseqlem5  24321  itg2addlem  24360  limcfval  24473  limcrcl  24475  ellimc2  24478  limcflf  24482  limcres  24487  limcun  24496  dvfval  24498  dvbss  24502  dvbsss  24503  perfdvf  24504  dvreslem  24510  dvres2lem  24511  dvcnp2  24521  dvnfval  24523  dvnff  24524  dvnf  24528  dvnbss  24529  dvnadd  24530  dvn2bss  24531  dvnres  24532  cpnfval  24533  cpnord  24536  dvaddbr  24539  dvmulbr  24540  dvnfre  24553  dvexp  24554  dvef  24581  c1liplem1  24597  c1lip2  24599  lhop1lem  24614  plyval  24788  elply  24790  elply2  24791  plyf  24793  plyss  24794  elplyr  24796  plyeq0lem  24805  plyeq0  24806  plypf1  24807  plyaddlem1  24808  plymullem1  24809  plyaddlem  24810  plymullem  24811  plysub  24814  coeeulem  24819  coeeq  24822  dgrlem  24824  coeidlem  24832  plyco  24836  coe0  24851  coesub  24852  dgrmulc  24866  dgrsub  24867  dgrcolem1  24868  dgrcolem2  24869  plymul0or  24875  dvnply2  24881  plycpn  24883  plydivlem3  24889  plydivlem4  24890  plydiveu  24892  plyremlem  24898  plyrem  24899  facth  24900  fta1lem  24901  quotcan  24903  vieta1lem2  24905  plyexmo  24907  elqaalem3  24915  qaa  24917  iaa  24919  aannenlem1  24922  aannenlem2  24923  aannenlem3  24924  taylfvallem1  24950  taylfval  24952  tayl0  24955  taylplem1  24956  taylply2  24961  taylply  24962  dvtaylp  24963  dvntaylp  24964  dvntaylp0  24965  taylthlem1  24966  taylthlem2  24967  ulmval  24973  ulmss  24990  ulmcn  24992  mtest  24997  pserulm  25015  psercn  25019  pserdvlem2  25021  abelth  25034  reefgim  25043  cxpcn2  25333  logbmpt  25372  logbfval  25374  lgamgulmlem5  25616  lgamgulmlem6  25617  lgamgulm2  25619  lgamcvglem  25623  ftalem7  25662  dchrfi  25837  cffldtocusgr  27235  isvcOLD  28360  cnaddabloOLD  28362  cnnvg  28459  cnnvs  28461  cnnvnm  28462  cncph  28600  hvmulex  28792  hfsmval  29519  hfmmval  29520  nmfnval  29657  nlfnval  29662  elcnfn  29663  ellnfn  29664  specval  29679  hhcnf  29686  lmlim  31264  esumcvg  31419  plymul02  31890  plymulx0  31891  signsplypnf  31894  signsply0  31895  breprexplemb  31976  breprexpnat  31979  vtsval  31982  circlemethnat  31986  circlevma  31987  circlemethhgt  31988  cvxpconn  32563  fwddifval  33697  fwddifnval  33698  ivthALT  33757  knoppcnlem5  33910  knoppcnlem8  33913  bj-inftyexpiinv  34584  bj-inftyexpidisj  34586  caures  35157  cntotbnd  35193  cnpwstotbnd  35194  rrnval  35224  cnaddcom  36227  elmnc  40011  mpaaeu  40025  itgoval  40036  itgocn  40039  rngunsnply  40048  binomcxplemnotnn0  40995  climexp  42187  xlimbr  42409  fuzxrpmcn  42410  xlimmnfvlem2  42415  xlimpnfvlem2  42419  mulcncff  42452  subcncff  42462  addcncff  42466  cncfuni  42468  divcncff  42473  dvsinax  42495  dvcosax  42508  dvnmptdivc  42520  dvnmptconst  42523  dvnxpaek  42524  dvnmul  42525  dvnprodlem3  42530  etransclem1  42817  etransclem2  42818  etransclem4  42820  etransclem13  42829  etransclem46  42862  fdivpm  44897  amgmlemALT  45271
  Copyright terms: Public domain W3C validator