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 12375. (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 2105  Vcvv 3495  cc 10524
This theorem was proved from axioms:  ax-cnex 10582
This theorem is referenced by:  reex  10617  cnelprrecn  10619  pnfex  10683  nnex  11633  zex  11979  qex  12350  addex  12377  mulex  12378  rlim  14842  rlimf  14848  rlimss  14849  elo12  14874  o1f  14876  o1dm  14877  cnso  15590  cnaddablx  18919  cnaddabl  18920  cnaddid  18921  cnaddinv  18922  cnfldbas  20479  cnfldcj  20482  cnfldds  20485  cnfldfun  20487  cnfldfunALT  20488  cnmsubglem  20538  cnmsgngrp  20653  psgninv  20656  lmbrf  21798  lmfss  21834  lmres  21838  lmcnp  21842  cnmet  23309  cncfval  23425  elcncf  23426  cncfcnvcn  23458  cnheibor  23488  cnlmodlem1  23669  tcphex  23749  tchnmfval  23760  tcphcph  23769  lmmbr2  23791  lmmbrf  23794  iscau2  23809  iscauf  23812  caucfil  23815  cmetcaulem  23820  caussi  23829  causs  23830  lmclimf  23836  mbff  24155  ismbf  24158  ismbfcn  24159  mbfconst  24163  mbfres  24174  mbfimaopn2  24187  cncombf  24188  cnmbf  24189  0plef  24202  0pledm  24203  itg1ge0  24216  mbfi1fseqlem5  24249  itg2addlem  24288  limcfval  24399  limcrcl  24401  ellimc2  24404  limcflf  24408  limcres  24413  limcun  24422  dvfval  24424  dvbss  24428  dvbsss  24429  perfdvf  24430  dvreslem  24436  dvres2lem  24437  dvcnp2  24446  dvnfval  24448  dvnff  24449  dvnf  24453  dvnbss  24454  dvnadd  24455  dvn2bss  24456  dvnres  24457  cpnfval  24458  cpnord  24461  dvaddbr  24464  dvmulbr  24465  dvnfre  24478  dvexp  24479  dvef  24506  c1liplem1  24522  c1lip2  24524  lhop1lem  24539  plyval  24712  elply  24714  elply2  24715  plyf  24717  plyss  24718  elplyr  24720  plyeq0lem  24729  plyeq0  24730  plypf1  24731  plyaddlem1  24732  plymullem1  24733  plyaddlem  24734  plymullem  24735  plysub  24738  coeeulem  24743  coeeq  24746  dgrlem  24748  coeidlem  24756  plyco  24760  coe0  24775  coesub  24776  dgrmulc  24790  dgrsub  24791  dgrcolem1  24792  dgrcolem2  24793  plymul0or  24799  dvnply2  24805  plycpn  24807  plydivlem3  24813  plydivlem4  24814  plydiveu  24816  plyremlem  24822  plyrem  24823  facth  24824  fta1lem  24825  quotcan  24827  vieta1lem2  24829  plyexmo  24831  elqaalem3  24839  qaa  24841  iaa  24843  aannenlem1  24846  aannenlem2  24847  aannenlem3  24848  taylfvallem1  24874  taylfval  24876  tayl0  24879  taylplem1  24880  taylply2  24885  taylply  24886  dvtaylp  24887  dvntaylp  24888  dvntaylp0  24889  taylthlem1  24890  taylthlem2  24891  ulmval  24897  ulmss  24914  ulmcn  24916  mtest  24921  pserulm  24939  psercn  24943  pserdvlem2  24945  abelth  24958  reefgim  24967  cxpcn2  25254  logbmpt  25293  logbfval  25295  lgamgulmlem5  25538  lgamgulmlem6  25539  lgamgulm2  25541  lgamcvglem  25545  ftalem7  25584  dchrfi  25759  cffldtocusgr  27157  isvcOLD  28284  cnaddabloOLD  28286  cnnvg  28383  cnnvs  28385  cnnvnm  28386  cncph  28524  hvmulex  28716  hfsmval  29443  hfmmval  29444  nmfnval  29581  nlfnval  29586  elcnfn  29587  ellnfn  29588  specval  29603  hhcnf  29610  lmlim  31090  esumcvg  31245  plymul02  31716  plymulx0  31717  signsplypnf  31720  signsply0  31721  breprexplemb  31802  breprexpnat  31805  vtsval  31808  circlemethnat  31812  circlevma  31813  circlemethhgt  31814  cvxpconn  32387  fwddifval  33521  fwddifnval  33522  ivthALT  33581  knoppcnlem5  33734  knoppcnlem8  33737  bj-inftyexpiinv  34383  bj-inftyexpidisj  34385  caures  34918  cntotbnd  34957  cnpwstotbnd  34958  rrnval  34988  cnaddcom  35990  elmnc  39616  mpaaeu  39630  itgoval  39641  itgocn  39644  rngunsnply  39653  binomcxplemnotnn0  40568  climexp  41766  xlimbr  41988  fuzxrpmcn  41989  xlimmnfvlem2  41994  xlimpnfvlem2  41998  mulcncff  42031  subcncff  42043  addcncff  42047  cncfuni  42049  divcncff  42054  dvsinax  42077  dvcosax  42091  dvnmptdivc  42103  dvnmptconst  42106  dvnxpaek  42107  dvnmul  42108  dvnprodlem3  42113  etransclem1  42401  etransclem2  42402  etransclem4  42404  etransclem13  42413  etransclem46  42446  fdivpm  44501  amgmlemALT  44802
  Copyright terms: Public domain W3C validator