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

Theorem c0ex 9634
Description: 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
c0ex  |-  0  e.  _V

Proof of Theorem c0ex
StepHypRef Expression
1 0cn 9632 . 2  |-  0  e.  CC
21elexi 3054 1  |-  0  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1886   _Vcvv 3044   CCcc 9534   0cc0 9536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-12 1932  ax-ext 2430  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-mulcl 9598  ax-i2m1 9604
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-v 3046
This theorem is referenced by:  ofsubeq0  10603  ofsubge0  10605  elnn0  10868  un0mulcl  10901  frnnn0supp  10920  frnnn0fsupp  10921  nn0ssz  10955  nn0ind-raph  11032  xaddval  11513  xmulval  11515  ser0f  12263  facnn  12458  fac0  12459  bcval  12486  prhash2ex  12573  snopiswrd  12678  wrdexb  12680  s1rn  12735  eqs1  12745  repsw1  12881  cshw1  12916  s1co  12925  wrdlen2i  13014  wrd2pr2op  13015  wwlktovf1  13025  sgnval  13144  iserge0  13717  sum0  13780  sumz  13781  fsumss  13784  fsumser  13789  isumless  13896  geomulcvg  13925  rpnnen2lem1  14260  ruclem4  14279  ruclem8  14282  ruclem11  14285  0bits  14406  gcdval  14463  lcmval  14548  lcmvalOLD  14549  lcmfpr  14593  lcmfunsnlem2  14606  prmreclem2  14854  prmreclem5  14857  vdwapun  14917  mgmnsgrpex  16658  odval  17173  odvalOLD  17176  odf  17179  odfOLD  17195  gexval  17220  gexvalOLD  17222  telgsumfz0  17615  telgsum  17617  srgbinom  17771  abvtrivd  18061  snifpsrbag  18583  psrbaglesupp  18585  psrbagaddcl  18587  psrbaglefi  18589  mplcoe5  18685  mplbas2  18687  ltbwe  18689  psrbag0  18710  psrbagev1  18726  cply1coe0bi  18887  m2cpminvid2lem  19771  pmatcollpw3fi1lem1  19803  pmatcollpw3fi1lem2  19804  pmatcollpw3fi1  19805  idpm2idmp  19818  prdsdsf  21375  prdsxmetlem  21376  prdsmet  21378  imasdsf1olem  21381  prdsbl  21499  xrge0gsumle  21844  xrge0tsms  21845  xrhmeo  21967  pcopt  22046  pcopt2  22047  pcoass  22048  rrxcph  22344  ovoliunnul  22453  ovolicc1  22462  vitalilem5  22563  mbfpos  22600  0pval  22622  0pledm  22624  i1f1lem  22640  i1f1  22641  itg11  22642  itg1addlem3  22649  itg1addlem4  22650  i1fres  22656  itg1climres  22665  mbfi1fseqlem4  22669  mbfi1fseqlem6  22671  mbfi1flimlem  22673  mbfi1flim  22674  xrge0f  22682  itg2ge0  22686  itg2uba  22694  itg2splitlem  22699  itg2monolem1  22701  itg2gt0  22711  itg2cnlem1  22712  ibl0  22737  iblcnlem1  22738  i1fibl  22758  itgeqa  22764  itgcn  22793  dvcmul  22891  dvcmulf  22892  dvexp3  22923  rolle  22935  dveq0  22945  dv11cn  22946  tdeglem4  23002  elply2  23143  elplyd  23149  ply1term  23151  ply0  23155  plyeq0  23158  plypf1  23159  plymullem  23163  dgrlt  23213  plymul0or  23227  dvply1  23230  plydivlem4  23242  elqaalem2  23266  elqaalem2OLD  23269  iaa  23274  aareccl  23275  aannenlem2  23278  tayl0  23310  taylpfval  23313  dvtaylp  23318  pserdvlem2  23376  abelthlem9  23388  logtayl  23598  cxplogb  23716  leibpilem2  23860  leibpi  23861  jensenlem2  23906  jensen  23907  amgmlem  23908  amgm  23909  igamval  23965  vmaval  24033  vmaf  24039  muval  24052  dchrelbas2  24158  dchrinvcl  24174  dchrptlem2  24186  lgseisenlem4  24273  pntrlog2bndlem4  24411  pntrlog2bndlem5  24412  padicval  24448  padicabv  24461  ostth1  24464  axlowdimlem8  24972  axlowdimlem9  24973  axlowdimlem10  24974  axlowdimlem11  24975  axlowdimlem12  24976  axlowdimlem13  24977  axlowdimlem17  24981  2trllemA  25273  2trllemH  25275  2trllemE  25276  2wlklemA  25277  wlkntrllem1  25282  wlkntrllem2  25283  wlkntrllem3  25284  2wlklem  25287  0spth  25294  constr1trl  25311  1pthon  25314  2pthlem2  25319  2wlklem1  25320  2pthon  25325  2pthon3v  25327  usgra2adedgwlkonALT  25337  usgra2wlkspthlem1  25340  usgra2wlkspthlem2  25341  constr3lem2  25367  constr3lem4  25368  constr3lem5  25369  constr3trllem1  25371  constr3trllem2  25372  clwwlkn2  25496  usg2wlkonot  25604  usg2wotspth  25605  0egra0rgra  25657  rusgranumwlkl1  25668  eupath  25702  occllem  26949  0cnfn  27626  0lnfn  27631  nmfn0  27633  nmcexi  27672  nlelchi  27707  xrge0infssOLD  28334  sgnsval  28484  sgnsf  28485  xrge0tsmsd  28541  xrge0iif1  28737  xrge0mulc1cn  28740  gsumesum  28873  esumpfinval  28889  esumpfinvalf  28890  ddeval1  29050  ddeval0  29051  ddemeas  29052  eulerpartlemt  29197  coinfliprv  29308  sgncl  29402  plymul02  29428  plymulx  29430  signsw0glem  29435  signsw0g  29438  signswmnd  29439  signswrid  29440  signstfvn  29451  cvmliftlem4  30004  cvmliftlem5  30005  poimirlem1  31934  poimirlem2  31935  poimirlem3  31936  poimirlem4  31937  poimirlem5  31938  poimirlem6  31939  poimirlem7  31940  poimirlem11  31944  poimirlem12  31945  poimirlem16  31949  poimirlem17  31950  poimirlem19  31952  poimirlem20  31953  poimirlem22  31955  poimirlem23  31956  poimirlem24  31957  poimirlem25  31958  poimirlem28  31961  poimirlem29  31962  poimirlem31  31964  poimirlem32  31965  poimir  31966  broucube  31967  mblfinlem2  31971  mblfinlem3  31972  ismblfin  31974  itg2addnclem  31986  itg2addnclem3  31988  itg2addnc  31989  ftc1anclem3  32012  ftc1anclem5  32014  ftc1anclem7  32016  ftc1anclem8  32017  ftc1anc  32018  dvacos  32022  prdsbnd  32118  heiborlem10  32145  renegclALT  32529  diophrw  35595  monotoddzzfi  35784  zindbi  35788  mncn0  35992  aaitgo  36022  flcidc  36034  dfrcl4  36262  fvrcllb0d  36279  fvrcllb0da  36280  iunrelexp0  36288  corclrcl  36293  relexp0idm  36301  dfrtrcl4  36324  corcltrcl  36325  cotrclrcl  36328  ofsubid  36667  lhe4.4ex1a  36672  dvsconst  36673  dvconstbi  36677  binomcxplemnn0  36692  binomcxplemdvbinom  36696  binomcxplemnotnn0  36699  n0p  37370  climrec  37675  dvnmptdivc  37807  dvnmul  37812  stoweidlem55  37910  fourierdlem62  38026  fourierdlem104  38068  fouriersw  38089  rrxbasefi  38146  ovnval2  38361  hoidmvval  38393  hoidmvlelem1  38411  el1fzopredsuc  38716  fun2dmnopgexmpl  39022  uspgrloopedg  39538  uspgrloopnb0  39539  uspgrloopvd2  39540  umgr2v2eedg  39544  umgr2v2e  39545  umgr2v2evd2  39547  2Wlklem  39645  usgra2adedglem1  39657  zlmodzxzel  40123  zlmodzxz0  40124  zlmodzxzscm  40125  zlmodzxzadd  40126  zlmodzxznm  40277  zlmodzxzldeplem  40278  zlmodzxzldeplem2  40281  blen0  40370  nn0sumshdiglemB  40418  ex-gt  40435  ex-gte  40436  aacllem  40527
  Copyright terms: Public domain W3C validator