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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8673 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   _Vcvv 2727   CCcc 8615
This theorem is referenced by:  reex  8708  nnex  9632  zex  9912  qex  10207  addex  10231  mulex  10232  pnfxr  10334  rlim  11846  rlimf  11852  rlimss  11853  elo12  11878  o1f  11880  o1dm  11881  cnso  12399  cnaddablx  14993  cnaddabl  14994  cnfldbas  16215  cnfldcj  16218  cnfldds  16221  cnmsubglem  16266  lmbrf  16822  lmfss  16856  lmres  16860  lmcnp  16864  cnmet  18113  cncfval  18224  elcncf  18225  cncfcnvcn  18256  cnheibor  18285  tchex  18481  tchnmfval  18491  tchcph  18499  lmmbr2  18517  lmmbrf  18520  iscau2  18535  iscauf  18538  caucfil  18541  cmetcaulem  18546  caussi  18555  causs  18556  lmclimf  18561  mbff  18814  ismbf  18817  ismbfcn  18818  mbfconst  18822  mbfres  18831  mbfimaopn2  18844  cncombf  18845  cnmbf  18846  0plef  18859  0pledm  18860  itg1ge0  18873  mbfi1fseqlem5  18906  itg2addlem  18945  limcfval  19054  limcrcl  19056  ellimc2  19059  limcflf  19063  limcres  19068  limcun  19077  dvfval  19079  dvbss  19083  dvbsss  19084  perfdvf  19085  dvfcn  19090  dvreslem  19091  dvres2lem  19092  dvcnp2  19101  dvnfval  19103  dvnff  19104  dvnf  19108  dvnbss  19109  dvnadd  19110  dvn2bss  19111  dvnres  19112  cpnfval  19113  cpnord  19116  dvaddbr  19119  dvmulbr  19120  dvaddf  19123  dvmulf  19124  dvcof  19129  dvnfre  19133  dvexp  19134  dvexp3  19157  dvef  19159  dvsincos  19160  dvlipcn  19173  c1liplem1  19175  c1lip2  19177  dv11cn  19180  lhop1lem  19192  plyval  19407  elply  19409  elply2  19410  plyf  19412  plyss  19413  elplyr  19415  plyeq0lem  19424  plyeq0  19425  plypf1  19426  plyaddlem1  19427  plymullem1  19428  plyaddlem  19429  plymullem  19430  plysub  19433  coeeulem  19438  coeeq  19441  dgrlem  19443  coeidlem  19451  plyco  19455  coe0  19469  coesub  19470  dgrmulc  19484  dgrsub  19485  dgrcolem1  19486  dgrcolem2  19487  plymul0or  19493  dvply1  19496  dvnply2  19499  plycpn  19501  plydivlem3  19507  plydivlem4  19508  plydiveu  19510  plyremlem  19516  plyrem  19517  facth  19518  fta1lem  19519  quotcan  19521  vieta1lem2  19523  plyexmo  19525  elqaalem3  19533  qaa  19535  iaa  19537  aannenlem1  19540  aannenlem2  19541  aannenlem3  19542  taylfvallem1  19568  taylfval  19570  tayl0  19573  taylplem1  19574  taylply2  19579  taylply  19580  dvtaylp  19581  dvntaylp  19582  dvntaylp0  19583  taylthlem1  19584  taylthlem2  19585  ulmval  19591  ulmss  19606  ulmcn  19608  mtest  19613  pserulm  19630  psercn  19634  pserdvlem2  19636  abelth  19649  reefgim  19658  pige3  19717  dvlog  19830  advlogexp  19834  logtayl  19839  dvcxp1  19950  dvcxp2  19951  cxpcn2  19954  dvatan  20063  efrlim  20096  ftalem7  20148  dchrfi  20326  logdivsum  20514  log2sumbnd  20525  cnaddablo  20847  ablomul  20852  vcoprne  20965  isvc  20967  cnnvg  21076  cnnvs  21079  cnnvnm  21080  cncph  21227  hvmulex  21421  hfsmval  22000  hfmmval  22001  nmfnval  22286  nlfnval  22291  elcnfn  22292  ellnfn  22293  specval  22308  hhcnf  22315  cvxpcon  22944  nZdef  24346  claddrv  24813  claddrvr  24814  sigadd  24815  zernpl  24819  addcomv  24821  addassv  24822  addidv2  24823  cnegvex2  24826  rnegvex2  24827  negveudr  24835  issubrv  24838  subclrvd  24840  ismulcv  24847  clsmulcv  24848  clsmulrv  24849  fnmulcv  24850  mulone  24851  distmlva  24854  distsava  24855  isdivcv2  24859  divclrvd  24861  ivthALT  25424  caures  25642  cntotbnd  25686  cnpwstotbnd  25687  rrnval  25717  elmnc  26507  mpaaeu  26521  itgoval  26532  itgocn  26535  rngunsnply  26544  cnmsgngrp  26602  lhe4.4ex1a  26712  expgrowthi  26716  expgrowth  26718  cnaddcom  27850
This theorem was proved from axioms:  ax-cnex 8673
  Copyright terms: Public domain W3C validator