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

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

Proof of Theorem cnex
StepHypRef Expression
1 ax-cnex 9036 1  |-  CC  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   _Vcvv 2948   CCcc 8978
This theorem is referenced by:  reex  9071  nnex  9996  zex  10281  qex  10576  addex  10600  mulex  10601  pnfxr  10703  rlim  12279  rlimf  12285  rlimss  12286  elo12  12311  o1f  12313  o1dm  12314  cnso  12836  cnaddablx  15471  cnaddabl  15472  cnfldbas  16697  cnfldcj  16700  cnfldds  16703  cnmsubglem  16751  lmbrf  17314  lmfss  17350  lmres  17354  lmcnp  17358  cnmet  18796  cncfval  18908  elcncf  18909  cncfcnvcn  18941  cnheibor  18970  tchex  19166  tchnmfval  19176  tchcph  19184  lmmbr2  19202  lmmbrf  19205  iscau2  19220  iscauf  19223  caucfil  19226  cmetcaulem  19231  caussi  19240  causs  19241  lmclimf  19246  mbff  19509  ismbf  19512  ismbfcn  19513  mbfconst  19517  mbfres  19526  mbfimaopn2  19539  cncombf  19540  cnmbf  19541  0plef  19554  0pledm  19555  itg1ge0  19568  mbfi1fseqlem5  19601  itg2addlem  19640  limcfval  19749  limcrcl  19751  ellimc2  19754  limcflf  19758  limcres  19763  limcun  19772  dvfval  19774  dvbss  19778  dvbsss  19779  perfdvf  19780  dvfcn  19785  dvreslem  19786  dvres2lem  19787  dvcnp2  19796  dvnfval  19798  dvnff  19799  dvnf  19803  dvnbss  19804  dvnadd  19805  dvn2bss  19806  dvnres  19807  cpnfval  19808  cpnord  19811  dvaddbr  19814  dvmulbr  19815  dvnfre  19828  dvexp  19829  dvexp3  19852  dvef  19854  dvsincos  19855  dvlipcn  19868  c1liplem1  19870  c1lip2  19872  dv11cn  19875  lhop1lem  19887  plyval  20102  elply  20104  elply2  20105  plyf  20107  plyss  20108  elplyr  20110  plyeq0lem  20119  plyeq0  20120  plypf1  20121  plyaddlem1  20122  plymullem1  20123  plyaddlem  20124  plymullem  20125  plysub  20128  coeeulem  20133  coeeq  20136  dgrlem  20138  coeidlem  20146  plyco  20150  coe0  20164  coesub  20165  dgrmulc  20179  dgrsub  20180  dgrcolem1  20181  dgrcolem2  20182  plymul0or  20188  dvply1  20191  dvnply2  20194  plycpn  20196  plydivlem3  20202  plydivlem4  20203  plydiveu  20205  plyremlem  20211  plyrem  20212  facth  20213  fta1lem  20214  quotcan  20216  vieta1lem2  20218  plyexmo  20220  elqaalem3  20228  qaa  20230  iaa  20232  aannenlem1  20235  aannenlem2  20236  aannenlem3  20237  taylfvallem1  20263  taylfval  20265  tayl0  20268  taylplem1  20269  taylply2  20274  taylply  20275  dvtaylp  20276  dvntaylp  20277  dvntaylp0  20278  taylthlem1  20279  taylthlem2  20280  ulmval  20286  ulmss  20303  ulmcn  20305  mtest  20310  pserulm  20328  psercn  20332  pserdvlem2  20334  abelth  20347  reefgim  20356  pige3  20415  dvlog  20532  advlogexp  20536  logtayl  20541  dvcxp1  20616  dvcxp2  20617  cxpcn2  20620  dvatan  20765  efrlim  20798  ftalem7  20851  dchrfi  21029  logdivsum  21217  log2sumbnd  21228  cnaddablo  21928  ablomul  21933  vcoprne  22048  isvc  22050  cnnvg  22159  cnnvs  22162  cnnvnm  22163  cncph  22310  hvmulex  22504  hfsmval  23231  hfmmval  23232  nmfnval  23369  nlfnval  23374  elcnfn  23375  ellnfn  23376  specval  23391  hhcnf  23398  lmlim  24323  esumcvg  24466  lgamgulmlem2  24804  lgamgulmlem5  24807  lgamgulmlem6  24808  lgamgulm2  24810  lgamcvglem  24814  cvxpcon  24919  dvreasin  26243  ivthALT  26292  caures  26420  cntotbnd  26459  cnpwstotbnd  26460  rrnval  26490  elmnc  27273  mpaaeu  27287  itgoval  27298  itgocn  27301  rngunsnply  27310  cnmsgngrp  27368  lhe4.4ex1a  27478  expgrowthi  27482  expgrowth  27484  climexp  27662  dvsinexp  27671  cnaddcom  29670
This theorem was proved from axioms:  ax-cnex 9036
  Copyright terms: Public domain W3C validator