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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8747 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   _Vcvv 2757   CCcc 8689
This theorem is referenced by:  reex  8782  nnex  9706  zex  9986  qex  10281  addex  10305  mulex  10306  pnfxr  10408  rlim  11920  rlimf  11926  rlimss  11927  elo12  11952  o1f  11954  o1dm  11955  cnso  12473  cnaddablx  15106  cnaddabl  15107  cnfldbas  16331  cnfldcj  16334  cnfldds  16337  cnmsubglem  16382  lmbrf  16938  lmfss  16972  lmres  16976  lmcnp  16980  cnmet  18229  cncfval  18340  elcncf  18341  cncfcnvcn  18372  cnheibor  18401  tchex  18597  tchnmfval  18607  tchcph  18615  lmmbr2  18633  lmmbrf  18636  iscau2  18651  iscauf  18654  caucfil  18657  cmetcaulem  18662  caussi  18671  causs  18672  lmclimf  18677  mbff  18930  ismbf  18933  ismbfcn  18934  mbfconst  18938  mbfres  18947  mbfimaopn2  18960  cncombf  18961  cnmbf  18962  0plef  18975  0pledm  18976  itg1ge0  18989  mbfi1fseqlem5  19022  itg2addlem  19061  limcfval  19170  limcrcl  19172  ellimc2  19175  limcflf  19179  limcres  19184  limcun  19193  dvfval  19195  dvbss  19199  dvbsss  19200  perfdvf  19201  dvfcn  19206  dvreslem  19207  dvres2lem  19208  dvcnp2  19217  dvnfval  19219  dvnff  19220  dvnf  19224  dvnbss  19225  dvnadd  19226  dvn2bss  19227  dvnres  19228  cpnfval  19229  cpnord  19232  dvaddbr  19235  dvmulbr  19236  dvaddf  19239  dvmulf  19240  dvcof  19245  dvnfre  19249  dvexp  19250  dvexp3  19273  dvef  19275  dvsincos  19276  dvlipcn  19289  c1liplem1  19291  c1lip2  19293  dv11cn  19296  lhop1lem  19308  plyval  19523  elply  19525  elply2  19526  plyf  19528  plyss  19529  elplyr  19531  plyeq0lem  19540  plyeq0  19541  plypf1  19542  plyaddlem1  19543  plymullem1  19544  plyaddlem  19545  plymullem  19546  plysub  19549  coeeulem  19554  coeeq  19557  dgrlem  19559  coeidlem  19567  plyco  19571  coe0  19585  coesub  19586  dgrmulc  19600  dgrsub  19601  dgrcolem1  19602  dgrcolem2  19603  plymul0or  19609  dvply1  19612  dvnply2  19615  plycpn  19617  plydivlem3  19623  plydivlem4  19624  plydiveu  19626  plyremlem  19632  plyrem  19633  facth  19634  fta1lem  19635  quotcan  19637  vieta1lem2  19639  plyexmo  19641  elqaalem3  19649  qaa  19651  iaa  19653  aannenlem1  19656  aannenlem2  19657  aannenlem3  19658  taylfvallem1  19684  taylfval  19686  tayl0  19689  taylplem1  19690  taylply2  19695  taylply  19696  dvtaylp  19697  dvntaylp  19698  dvntaylp0  19699  taylthlem1  19700  taylthlem2  19701  ulmval  19707  ulmss  19722  ulmcn  19724  mtest  19729  pserulm  19746  psercn  19750  pserdvlem2  19752  abelth  19765  reefgim  19774  pige3  19833  dvlog  19946  advlogexp  19950  logtayl  19955  dvcxp1  20030  dvcxp2  20031  cxpcn2  20034  dvatan  20179  efrlim  20212  ftalem7  20264  dchrfi  20442  logdivsum  20630  log2sumbnd  20641  cnaddablo  20963  ablomul  20968  vcoprne  21081  isvc  21083  cnnvg  21192  cnnvs  21195  cnnvnm  21196  cncph  21343  hvmulex  21537  hfsmval  22116  hfmmval  22117  nmfnval  22402  nlfnval  22407  elcnfn  22408  ellnfn  22409  specval  22424  hhcnf  22431  cvxpcon  23131  nZdef  24533  claddrv  25000  claddrvr  25001  sigadd  25002  zernpl  25006  addcomv  25008  addassv  25009  addidv2  25010  cnegvex2  25013  rnegvex2  25014  negveudr  25022  issubrv  25025  subclrvd  25027  ismulcv  25034  clsmulcv  25035  clsmulrv  25036  fnmulcv  25037  mulone  25038  distmlva  25041  distsava  25042  isdivcv2  25046  divclrvd  25048  ivthALT  25611  caures  25829  cntotbnd  25873  cnpwstotbnd  25874  rrnval  25904  elmnc  26694  mpaaeu  26708  itgoval  26719  itgocn  26722  rngunsnply  26731  cnmsgngrp  26789  lhe4.4ex1a  26899  expgrowthi  26903  expgrowth  26905  cnaddcom  28312
This theorem was proved from axioms:  ax-cnex 8747
  Copyright terms: Public domain W3C validator