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

Theorem cnex 8814
Description: Alias for ax-cnex 8789. See also cnexALT 10346. (Contributed by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
cnex  |-  CC  e.  _V

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8789 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1685   _Vcvv 2790   CCcc 8731
This theorem is referenced by:  reex  8824  nnex  9748  zex  10029  qex  10324  addex  10348  mulex  10349  pnfxr  10451  rlim  11964  rlimf  11970  rlimss  11971  elo12  11996  o1f  11998  o1dm  11999  cnso  12520  cnaddablx  15153  cnaddabl  15154  cnfldbas  16378  cnfldcj  16381  cnfldds  16384  cnmsubglem  16429  lmbrf  16985  lmfss  17019  lmres  17023  lmcnp  17027  cnmet  18276  cncfval  18387  elcncf  18388  cncfcnvcn  18419  cnheibor  18448  tchex  18644  tchnmfval  18654  tchcph  18662  lmmbr2  18680  lmmbrf  18683  iscau2  18698  iscauf  18701  caucfil  18704  cmetcaulem  18709  caussi  18718  causs  18719  lmclimf  18724  mbff  18977  ismbf  18980  ismbfcn  18981  mbfconst  18985  mbfres  18994  mbfimaopn2  19007  cncombf  19008  cnmbf  19009  0plef  19022  0pledm  19023  itg1ge0  19036  mbfi1fseqlem5  19069  itg2addlem  19108  limcfval  19217  limcrcl  19219  ellimc2  19222  limcflf  19226  limcres  19231  limcun  19240  dvfval  19242  dvbss  19246  dvbsss  19247  perfdvf  19248  dvfcn  19253  dvreslem  19254  dvres2lem  19255  dvcnp2  19264  dvnfval  19266  dvnff  19267  dvnf  19271  dvnbss  19272  dvnadd  19273  dvn2bss  19274  dvnres  19275  cpnfval  19276  cpnord  19279  dvaddbr  19282  dvmulbr  19283  dvaddf  19286  dvmulf  19287  dvcof  19292  dvnfre  19296  dvexp  19297  dvexp3  19320  dvef  19322  dvsincos  19323  dvlipcn  19336  c1liplem1  19338  c1lip2  19340  dv11cn  19343  lhop1lem  19355  plyval  19570  elply  19572  elply2  19573  plyf  19575  plyss  19576  elplyr  19578  plyeq0lem  19587  plyeq0  19588  plypf1  19589  plyaddlem1  19590  plymullem1  19591  plyaddlem  19592  plymullem  19593  plysub  19596  coeeulem  19601  coeeq  19604  dgrlem  19606  coeidlem  19614  plyco  19618  coe0  19632  coesub  19633  dgrmulc  19647  dgrsub  19648  dgrcolem1  19649  dgrcolem2  19650  plymul0or  19656  dvply1  19659  dvnply2  19662  plycpn  19664  plydivlem3  19670  plydivlem4  19671  plydiveu  19673  plyremlem  19679  plyrem  19680  facth  19681  fta1lem  19682  quotcan  19684  vieta1lem2  19686  plyexmo  19688  elqaalem3  19696  qaa  19698  iaa  19700  aannenlem1  19703  aannenlem2  19704  aannenlem3  19705  taylfvallem1  19731  taylfval  19733  tayl0  19736  taylplem1  19737  taylply2  19742  taylply  19743  dvtaylp  19744  dvntaylp  19745  dvntaylp0  19746  taylthlem1  19747  taylthlem2  19748  ulmval  19754  ulmss  19769  ulmcn  19771  mtest  19776  pserulm  19793  psercn  19797  pserdvlem2  19799  abelth  19812  reefgim  19821  pige3  19880  dvlog  19993  advlogexp  19997  logtayl  20002  dvcxp1  20077  dvcxp2  20078  cxpcn2  20081  dvatan  20226  efrlim  20259  ftalem7  20311  dchrfi  20489  logdivsum  20677  log2sumbnd  20688  cnaddablo  21010  ablomul  21015  vcoprne  21128  isvc  21130  cnnvg  21239  cnnvs  21242  cnnvnm  21243  cncph  21390  hvmulex  21584  hfsmval  22311  hfmmval  22312  nmfnval  22449  nlfnval  22454  elcnfn  22455  ellnfn  22456  specval  22471  hhcnf  22478  cvxpcon  23178  nZdef  24580  claddrv  25047  claddrvr  25048  sigadd  25049  zernpl  25053  addcomv  25055  addassv  25056  addidv2  25057  cnegvex2  25060  rnegvex2  25061  negveudr  25069  issubrv  25072  subclrvd  25074  ismulcv  25081  clsmulcv  25082  clsmulrv  25083  fnmulcv  25084  mulone  25085  distmlva  25088  distsava  25089  isdivcv2  25093  divclrvd  25095  ivthALT  25658  caures  25876  cntotbnd  25920  cnpwstotbnd  25921  rrnval  25951  elmnc  26741  mpaaeu  26755  itgoval  26766  itgocn  26769  rngunsnply  26778  cnmsgngrp  26836  lhe4.4ex1a  26946  expgrowthi  26950  expgrowth  26952  climexp  27131  dvsinexp  27140  cnaddcom  28429
This theorem was proved from axioms:  ax-cnex 8789
  Copyright terms: Public domain W3C validator