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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 8980 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   _Vcvv 2900   CCcc 8922
This theorem is referenced by:  reex  9015  nnex  9939  zex  10224  qex  10519  addex  10543  mulex  10544  pnfxr  10646  rlim  12217  rlimf  12223  rlimss  12224  elo12  12249  o1f  12251  o1dm  12252  cnso  12774  cnaddablx  15409  cnaddabl  15410  cnfldbas  16631  cnfldcj  16634  cnfldds  16637  cnmsubglem  16685  lmbrf  17247  lmfss  17283  lmres  17287  lmcnp  17291  cnmet  18678  cncfval  18790  elcncf  18791  cncfcnvcn  18823  cnheibor  18852  tchex  19048  tchnmfval  19058  tchcph  19066  lmmbr2  19084  lmmbrf  19087  iscau2  19102  iscauf  19105  caucfil  19108  cmetcaulem  19113  caussi  19122  causs  19123  lmclimf  19128  mbff  19387  ismbf  19390  ismbfcn  19391  mbfconst  19395  mbfres  19404  mbfimaopn2  19417  cncombf  19418  cnmbf  19419  0plef  19432  0pledm  19433  itg1ge0  19446  mbfi1fseqlem5  19479  itg2addlem  19518  limcfval  19627  limcrcl  19629  ellimc2  19632  limcflf  19636  limcres  19641  limcun  19650  dvfval  19652  dvbss  19656  dvbsss  19657  perfdvf  19658  dvfcn  19663  dvreslem  19664  dvres2lem  19665  dvcnp2  19674  dvnfval  19676  dvnff  19677  dvnf  19681  dvnbss  19682  dvnadd  19683  dvn2bss  19684  dvnres  19685  cpnfval  19686  cpnord  19689  dvaddbr  19692  dvmulbr  19693  dvnfre  19706  dvexp  19707  dvexp3  19730  dvef  19732  dvsincos  19733  dvlipcn  19746  c1liplem1  19748  c1lip2  19750  dv11cn  19753  lhop1lem  19765  plyval  19980  elply  19982  elply2  19983  plyf  19985  plyss  19986  elplyr  19988  plyeq0lem  19997  plyeq0  19998  plypf1  19999  plyaddlem1  20000  plymullem1  20001  plyaddlem  20002  plymullem  20003  plysub  20006  coeeulem  20011  coeeq  20014  dgrlem  20016  coeidlem  20024  plyco  20028  coe0  20042  coesub  20043  dgrmulc  20057  dgrsub  20058  dgrcolem1  20059  dgrcolem2  20060  plymul0or  20066  dvply1  20069  dvnply2  20072  plycpn  20074  plydivlem3  20080  plydivlem4  20081  plydiveu  20083  plyremlem  20089  plyrem  20090  facth  20091  fta1lem  20092  quotcan  20094  vieta1lem2  20096  plyexmo  20098  elqaalem3  20106  qaa  20108  iaa  20110  aannenlem1  20113  aannenlem2  20114  aannenlem3  20115  taylfvallem1  20141  taylfval  20143  tayl0  20146  taylplem1  20147  taylply2  20152  taylply  20153  dvtaylp  20154  dvntaylp  20155  dvntaylp0  20156  taylthlem1  20157  taylthlem2  20158  ulmval  20164  ulmss  20181  ulmcn  20183  mtest  20188  pserulm  20206  psercn  20210  pserdvlem2  20212  abelth  20225  reefgim  20234  pige3  20293  dvlog  20410  advlogexp  20414  logtayl  20419  dvcxp1  20494  dvcxp2  20495  cxpcn2  20498  dvatan  20643  efrlim  20676  ftalem7  20729  dchrfi  20907  logdivsum  21095  log2sumbnd  21106  cnaddablo  21787  ablomul  21792  vcoprne  21907  isvc  21909  cnnvg  22018  cnnvs  22021  cnnvnm  22022  cncph  22169  hvmulex  22363  hfsmval  23090  hfmmval  23091  nmfnval  23228  nlfnval  23233  elcnfn  23234  ellnfn  23235  specval  23250  hhcnf  23257  lmlim  24138  esumcvg  24273  lgamgulmlem2  24594  lgamgulmlem5  24597  lgamgulmlem6  24598  lgamgulm2  24600  lgamcvglem  24604  cvxpcon  24709  dvreasin  25981  ivthALT  26030  caures  26158  cntotbnd  26197  cnpwstotbnd  26198  rrnval  26228  elmnc  27011  mpaaeu  27025  itgoval  27036  itgocn  27039  rngunsnply  27048  cnmsgngrp  27106  lhe4.4ex1a  27216  expgrowthi  27220  expgrowth  27222  climexp  27400  dvsinexp  27409  cnaddcom  29087
This theorem was proved from axioms:  ax-cnex 8980
  Copyright terms: Public domain W3C validator