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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 9002 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   _Vcvv 2916   CCcc 8944
This theorem is referenced by:  reex  9037  nnex  9962  zex  10247  qex  10542  addex  10566  mulex  10567  pnfxr  10669  rlim  12244  rlimf  12250  rlimss  12251  elo12  12276  o1f  12278  o1dm  12279  cnso  12801  cnaddablx  15436  cnaddabl  15437  cnfldbas  16662  cnfldcj  16665  cnfldds  16668  cnmsubglem  16716  lmbrf  17278  lmfss  17314  lmres  17318  lmcnp  17322  cnmet  18759  cncfval  18871  elcncf  18872  cncfcnvcn  18904  cnheibor  18933  tchex  19129  tchnmfval  19139  tchcph  19147  lmmbr2  19165  lmmbrf  19168  iscau2  19183  iscauf  19186  caucfil  19189  cmetcaulem  19194  caussi  19203  causs  19204  lmclimf  19209  mbff  19472  ismbf  19475  ismbfcn  19476  mbfconst  19480  mbfres  19489  mbfimaopn2  19502  cncombf  19503  cnmbf  19504  0plef  19517  0pledm  19518  itg1ge0  19531  mbfi1fseqlem5  19564  itg2addlem  19603  limcfval  19712  limcrcl  19714  ellimc2  19717  limcflf  19721  limcres  19726  limcun  19735  dvfval  19737  dvbss  19741  dvbsss  19742  perfdvf  19743  dvfcn  19748  dvreslem  19749  dvres2lem  19750  dvcnp2  19759  dvnfval  19761  dvnff  19762  dvnf  19766  dvnbss  19767  dvnadd  19768  dvn2bss  19769  dvnres  19770  cpnfval  19771  cpnord  19774  dvaddbr  19777  dvmulbr  19778  dvnfre  19791  dvexp  19792  dvexp3  19815  dvef  19817  dvsincos  19818  dvlipcn  19831  c1liplem1  19833  c1lip2  19835  dv11cn  19838  lhop1lem  19850  plyval  20065  elply  20067  elply2  20068  plyf  20070  plyss  20071  elplyr  20073  plyeq0lem  20082  plyeq0  20083  plypf1  20084  plyaddlem1  20085  plymullem1  20086  plyaddlem  20087  plymullem  20088  plysub  20091  coeeulem  20096  coeeq  20099  dgrlem  20101  coeidlem  20109  plyco  20113  coe0  20127  coesub  20128  dgrmulc  20142  dgrsub  20143  dgrcolem1  20144  dgrcolem2  20145  plymul0or  20151  dvply1  20154  dvnply2  20157  plycpn  20159  plydivlem3  20165  plydivlem4  20166  plydiveu  20168  plyremlem  20174  plyrem  20175  facth  20176  fta1lem  20177  quotcan  20179  vieta1lem2  20181  plyexmo  20183  elqaalem3  20191  qaa  20193  iaa  20195  aannenlem1  20198  aannenlem2  20199  aannenlem3  20200  taylfvallem1  20226  taylfval  20228  tayl0  20231  taylplem1  20232  taylply2  20237  taylply  20238  dvtaylp  20239  dvntaylp  20240  dvntaylp0  20241  taylthlem1  20242  taylthlem2  20243  ulmval  20249  ulmss  20266  ulmcn  20268  mtest  20273  pserulm  20291  psercn  20295  pserdvlem2  20297  abelth  20310  reefgim  20319  pige3  20378  dvlog  20495  advlogexp  20499  logtayl  20504  dvcxp1  20579  dvcxp2  20580  cxpcn2  20583  dvatan  20728  efrlim  20761  ftalem7  20814  dchrfi  20992  logdivsum  21180  log2sumbnd  21191  cnaddablo  21891  ablomul  21896  vcoprne  22011  isvc  22013  cnnvg  22122  cnnvs  22125  cnnvnm  22126  cncph  22273  hvmulex  22467  hfsmval  23194  hfmmval  23195  nmfnval  23332  nlfnval  23337  elcnfn  23338  ellnfn  23339  specval  23354  hhcnf  23361  lmlim  24286  esumcvg  24429  lgamgulmlem2  24767  lgamgulmlem5  24770  lgamgulmlem6  24771  lgamgulm2  24773  lgamcvglem  24777  cvxpcon  24882  dvreasin  26179  ivthALT  26228  caures  26356  cntotbnd  26395  cnpwstotbnd  26396  rrnval  26426  elmnc  27209  mpaaeu  27223  itgoval  27234  itgocn  27237  rngunsnply  27246  cnmsgngrp  27304  lhe4.4ex1a  27414  expgrowthi  27418  expgrowth  27420  climexp  27598  dvsinexp  27607  cnaddcom  29454
This theorem was proved from axioms:  ax-cnex 9002
  Copyright terms: Public domain W3C validator