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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8793 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788   CCcc 8735
This theorem is referenced by:  reex  8828  nnex  9752  zex  10033  qex  10328  addex  10352  mulex  10353  pnfxr  10455  rlim  11969  rlimf  11975  rlimss  11976  elo12  12001  o1f  12003  o1dm  12004  cnso  12525  cnaddablx  15158  cnaddabl  15159  cnfldbas  16383  cnfldcj  16386  cnfldds  16389  cnmsubglem  16434  lmbrf  16990  lmfss  17024  lmres  17028  lmcnp  17032  cnmet  18281  cncfval  18392  elcncf  18393  cncfcnvcn  18424  cnheibor  18453  tchex  18649  tchnmfval  18659  tchcph  18667  lmmbr2  18685  lmmbrf  18688  iscau2  18703  iscauf  18706  caucfil  18709  cmetcaulem  18714  caussi  18723  causs  18724  lmclimf  18729  mbff  18982  ismbf  18985  ismbfcn  18986  mbfconst  18990  mbfres  18999  mbfimaopn2  19012  cncombf  19013  cnmbf  19014  0plef  19027  0pledm  19028  itg1ge0  19041  mbfi1fseqlem5  19074  itg2addlem  19113  limcfval  19222  limcrcl  19224  ellimc2  19227  limcflf  19231  limcres  19236  limcun  19245  dvfval  19247  dvbss  19251  dvbsss  19252  perfdvf  19253  dvfcn  19258  dvreslem  19259  dvres2lem  19260  dvcnp2  19269  dvnfval  19271  dvnff  19272  dvnf  19276  dvnbss  19277  dvnadd  19278  dvn2bss  19279  dvnres  19280  cpnfval  19281  cpnord  19284  dvaddbr  19287  dvmulbr  19288  dvaddf  19291  dvmulf  19292  dvcof  19297  dvnfre  19301  dvexp  19302  dvexp3  19325  dvef  19327  dvsincos  19328  dvlipcn  19341  c1liplem1  19343  c1lip2  19345  dv11cn  19348  lhop1lem  19360  plyval  19575  elply  19577  elply2  19578  plyf  19580  plyss  19581  elplyr  19583  plyeq0lem  19592  plyeq0  19593  plypf1  19594  plyaddlem1  19595  plymullem1  19596  plyaddlem  19597  plymullem  19598  plysub  19601  coeeulem  19606  coeeq  19609  dgrlem  19611  coeidlem  19619  plyco  19623  coe0  19637  coesub  19638  dgrmulc  19652  dgrsub  19653  dgrcolem1  19654  dgrcolem2  19655  plymul0or  19661  dvply1  19664  dvnply2  19667  plycpn  19669  plydivlem3  19675  plydivlem4  19676  plydiveu  19678  plyremlem  19684  plyrem  19685  facth  19686  fta1lem  19687  quotcan  19689  vieta1lem2  19691  plyexmo  19693  elqaalem3  19701  qaa  19703  iaa  19705  aannenlem1  19708  aannenlem2  19709  aannenlem3  19710  taylfvallem1  19736  taylfval  19738  tayl0  19741  taylplem1  19742  taylply2  19747  taylply  19748  dvtaylp  19749  dvntaylp  19750  dvntaylp0  19751  taylthlem1  19752  taylthlem2  19753  ulmval  19759  ulmss  19774  ulmcn  19776  mtest  19781  pserulm  19798  psercn  19802  pserdvlem2  19804  abelth  19817  reefgim  19826  pige3  19885  dvlog  19998  advlogexp  20002  logtayl  20007  dvcxp1  20082  dvcxp2  20083  cxpcn2  20086  dvatan  20231  efrlim  20264  ftalem7  20316  dchrfi  20494  logdivsum  20682  log2sumbnd  20693  cnaddablo  21017  ablomul  21022  vcoprne  21135  isvc  21137  cnnvg  21246  cnnvs  21249  cnnvnm  21250  cncph  21397  hvmulex  21591  hfsmval  22318  hfmmval  22319  nmfnval  22456  nlfnval  22461  elcnfn  22462  ellnfn  22463  specval  22478  hhcnf  22485  lmlim  23371  esumcvg  23454  cvxpcon  23773  dvreasin  24923  nZdef  25180  claddrv  25647  claddrvr  25648  sigadd  25649  zernpl  25653  addcomv  25655  addassv  25656  addidv2  25657  cnegvex2  25660  rnegvex2  25661  negveudr  25669  issubrv  25672  subclrvd  25674  ismulcv  25681  clsmulcv  25682  clsmulrv  25683  fnmulcv  25684  mulone  25685  distmlva  25688  distsava  25689  isdivcv2  25693  divclrvd  25695  ivthALT  26258  caures  26476  cntotbnd  26520  cnpwstotbnd  26521  rrnval  26551  elmnc  27341  mpaaeu  27355  itgoval  27366  itgocn  27369  rngunsnply  27378  cnmsgngrp  27436  lhe4.4ex1a  27546  expgrowthi  27550  expgrowth  27552  climexp  27731  dvsinexp  27740  cnaddcom  29161
This theorem was proved from axioms:  ax-cnex 8793
  Copyright terms: Public domain W3C validator