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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8809 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   _Vcvv 2801   CCcc 8751
This theorem is referenced by:  reex  8844  nnex  9768  zex  10049  qex  10344  addex  10368  mulex  10369  pnfxr  10471  rlim  11985  rlimf  11991  rlimss  11992  elo12  12017  o1f  12019  o1dm  12020  cnso  12541  cnaddablx  15174  cnaddabl  15175  cnfldbas  16399  cnfldcj  16402  cnfldds  16405  cnmsubglem  16450  lmbrf  17006  lmfss  17040  lmres  17044  lmcnp  17048  cnmet  18297  cncfval  18408  elcncf  18409  cncfcnvcn  18440  cnheibor  18469  tchex  18665  tchnmfval  18675  tchcph  18683  lmmbr2  18701  lmmbrf  18704  iscau2  18719  iscauf  18722  caucfil  18725  cmetcaulem  18730  caussi  18739  causs  18740  lmclimf  18745  mbff  18998  ismbf  19001  ismbfcn  19002  mbfconst  19006  mbfres  19015  mbfimaopn2  19028  cncombf  19029  cnmbf  19030  0plef  19043  0pledm  19044  itg1ge0  19057  mbfi1fseqlem5  19090  itg2addlem  19129  limcfval  19238  limcrcl  19240  ellimc2  19243  limcflf  19247  limcres  19252  limcun  19261  dvfval  19263  dvbss  19267  dvbsss  19268  perfdvf  19269  dvfcn  19274  dvreslem  19275  dvres2lem  19276  dvcnp2  19285  dvnfval  19287  dvnff  19288  dvnf  19292  dvnbss  19293  dvnadd  19294  dvn2bss  19295  dvnres  19296  cpnfval  19297  cpnord  19300  dvaddbr  19303  dvmulbr  19304  dvaddf  19307  dvmulf  19308  dvcof  19313  dvnfre  19317  dvexp  19318  dvexp3  19341  dvef  19343  dvsincos  19344  dvlipcn  19357  c1liplem1  19359  c1lip2  19361  dv11cn  19364  lhop1lem  19376  plyval  19591  elply  19593  elply2  19594  plyf  19596  plyss  19597  elplyr  19599  plyeq0lem  19608  plyeq0  19609  plypf1  19610  plyaddlem1  19611  plymullem1  19612  plyaddlem  19613  plymullem  19614  plysub  19617  coeeulem  19622  coeeq  19625  dgrlem  19627  coeidlem  19635  plyco  19639  coe0  19653  coesub  19654  dgrmulc  19668  dgrsub  19669  dgrcolem1  19670  dgrcolem2  19671  plymul0or  19677  dvply1  19680  dvnply2  19683  plycpn  19685  plydivlem3  19691  plydivlem4  19692  plydiveu  19694  plyremlem  19700  plyrem  19701  facth  19702  fta1lem  19703  quotcan  19705  vieta1lem2  19707  plyexmo  19709  elqaalem3  19717  qaa  19719  iaa  19721  aannenlem1  19724  aannenlem2  19725  aannenlem3  19726  taylfvallem1  19752  taylfval  19754  tayl0  19757  taylplem1  19758  taylply2  19763  taylply  19764  dvtaylp  19765  dvntaylp  19766  dvntaylp0  19767  taylthlem1  19768  taylthlem2  19769  ulmval  19775  ulmss  19790  ulmcn  19792  mtest  19797  pserulm  19814  psercn  19818  pserdvlem2  19820  abelth  19833  reefgim  19842  pige3  19901  dvlog  20014  advlogexp  20018  logtayl  20023  dvcxp1  20098  dvcxp2  20099  cxpcn2  20102  dvatan  20247  efrlim  20280  ftalem7  20332  dchrfi  20510  logdivsum  20698  log2sumbnd  20709  cnaddablo  21033  ablomul  21038  vcoprne  21151  isvc  21153  cnnvg  21262  cnnvs  21265  cnnvnm  21266  cncph  21413  hvmulex  21607  hfsmval  22334  hfmmval  22335  nmfnval  22472  nlfnval  22477  elcnfn  22478  ellnfn  22479  specval  22494  hhcnf  22501  lmlim  23386  esumcvg  23469  cvxpcon  23788  dvreasin  25026  nZdef  25283  claddrv  25750  claddrvr  25751  sigadd  25752  zernpl  25756  addcomv  25758  addassv  25759  addidv2  25760  cnegvex2  25763  rnegvex2  25764  negveudr  25772  issubrv  25775  subclrvd  25777  ismulcv  25784  clsmulcv  25785  clsmulrv  25786  fnmulcv  25787  mulone  25788  distmlva  25791  distsava  25792  isdivcv2  25796  divclrvd  25798  ivthALT  26361  caures  26579  cntotbnd  26623  cnpwstotbnd  26624  rrnval  26654  elmnc  27444  mpaaeu  27458  itgoval  27469  itgocn  27472  rngunsnply  27481  cnmsgngrp  27539  lhe4.4ex1a  27649  expgrowthi  27653  expgrowth  27655  climexp  27834  dvsinexp  27843  cnaddcom  29783
This theorem was proved from axioms:  ax-cnex 8809
  Copyright terms: Public domain W3C validator