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

Theorem c0ex 9626
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 9624 . 2  |-  0  e.  CC
21elexi 3088 1  |-  0  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1867   _Vcvv 3078   CCcc 9526   0cc0 9528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-12 1904  ax-ext 2398  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-mulcl 9590  ax-i2m1 9596
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-v 3080
This theorem is referenced by:  ofsubeq0  10595  ofsubge0  10597  elnn0  10860  un0mulcl  10893  frnnn0supp  10912  frnnn0fsupp  10913  nn0ssz  10947  nn0ind-raph  11024  xaddval  11505  xmulval  11507  ser0f  12252  facnn  12447  fac0  12448  bcval  12475  prhash2ex  12562  snopiswrd  12657  wrdexb  12659  s1rn  12714  eqs1  12724  repsw1  12860  cshw1  12895  s1co  12904  wrdlen2i  12989  wrd2pr2op  12990  wwlktovf1  13000  sgnval  13119  iserge0  13691  sum0  13754  sumz  13755  fsumss  13758  fsumser  13763  isumless  13870  geomulcvg  13899  rpnnen2lem1  14234  ruclem4  14253  ruclem8  14256  ruclem11  14259  0bits  14376  gcdval  14433  lcmval  14515  lcmvalOLD  14516  lcmfpr  14560  lcmfunsnlem2  14573  prmreclem2  14813  prmreclem5  14816  vdwapun  14876  mgmnsgrpex  16609  odval  17118  odf  17121  gexval  17158  telgsumfz0  17550  telgsum  17552  srgbinom  17706  abvtrivd  17996  snifpsrbag  18518  psrbaglesupp  18520  psrbagaddcl  18522  psrbaglefi  18524  mplcoe5  18620  mplbas2  18622  ltbwe  18624  psrbag0  18645  psrbagev1  18661  cply1coe0bi  18822  m2cpminvid2lem  19702  pmatcollpw3fi1lem1  19734  pmatcollpw3fi1lem2  19735  pmatcollpw3fi1  19736  idpm2idmp  19749  prdsdsf  21306  prdsxmetlem  21307  prdsmet  21309  imasdsf1olem  21312  prdsbl  21430  xrge0gsumle  21755  xrge0tsms  21756  xrhmeo  21863  pcopt  21939  pcopt2  21940  pcoass  21941  rrxcph  22237  ovoliunnul  22334  ovolicc1  22343  vitalilem5  22444  mbfpos  22481  0pval  22503  0pledm  22505  i1f1lem  22521  i1f1  22522  itg11  22523  itg1addlem3  22530  itg1addlem4  22531  i1fres  22537  itg1climres  22546  mbfi1fseqlem4  22550  mbfi1fseqlem6  22552  mbfi1flimlem  22554  mbfi1flim  22555  xrge0f  22563  itg2ge0  22567  itg2uba  22575  itg2splitlem  22580  itg2monolem1  22582  itg2gt0  22592  itg2cnlem1  22593  ibl0  22618  iblcnlem1  22619  i1fibl  22639  itgeqa  22645  itgcn  22674  dvcmul  22772  dvcmulf  22773  dvexp3  22804  rolle  22816  dveq0  22826  dv11cn  22827  tdeglem4  22883  elply2  23015  elplyd  23021  ply1term  23023  ply0  23027  plyeq0  23030  plypf1  23031  plymullem  23035  dgrlt  23085  plymul0or  23099  dvply1  23102  plydivlem4  23114  elqaalem2  23138  iaa  23143  aareccl  23144  aannenlem2  23147  tayl0  23179  taylpfval  23182  dvtaylp  23187  pserdvlem2  23245  abelthlem9  23257  logtayl  23467  cxplogb  23585  leibpilem2  23729  leibpi  23730  jensenlem2  23775  jensen  23776  amgmlem  23777  amgm  23778  igamval  23834  vmaval  23900  vmaf  23906  muval  23919  dchrelbas2  24025  dchrinvcl  24041  dchrptlem2  24053  lgseisenlem4  24140  pntrlog2bndlem4  24278  pntrlog2bndlem5  24279  padicval  24315  padicabv  24328  ostth1  24331  axlowdimlem8  24822  axlowdimlem9  24823  axlowdimlem10  24824  axlowdimlem11  24825  axlowdimlem12  24826  axlowdimlem13  24827  axlowdimlem17  24831  2trllemA  25122  2trllemH  25124  2trllemE  25125  2wlklemA  25126  wlkntrllem1  25131  wlkntrllem2  25132  wlkntrllem3  25133  2wlklem  25136  0spth  25143  constr1trl  25160  1pthon  25163  2pthlem2  25168  2wlklem1  25169  2pthon  25174  2pthon3v  25176  usgra2adedgwlkonALT  25186  usgra2wlkspthlem1  25189  usgra2wlkspthlem2  25190  constr3lem2  25216  constr3lem4  25217  constr3lem5  25218  constr3trllem1  25220  constr3trllem2  25221  clwwlkn2  25345  usg2wlkonot  25453  usg2wotspth  25454  0egra0rgra  25506  rusgranumwlkl1  25517  eupath  25551  occllem  26788  0cnfn  27465  0lnfn  27470  nmfn0  27472  nmcexi  27511  nlelchi  27546  xrge0infss  28178  sgnsval  28326  sgnsf  28327  xrge0tsmsd  28384  xrge0iif1  28580  xrge0mulc1cn  28583  gsumesum  28716  esumpfinval  28732  esumpfinvalf  28733  ddeval1  28893  ddeval0  28894  ddemeas  28895  eulerpartlemt  29027  coinfliprv  29138  sgncl  29194  plymul02  29220  plymulx  29222  signsw0glem  29227  signsw0g  29230  signswmnd  29231  signswrid  29232  signstfvn  29243  cvmliftlem4  29796  cvmliftlem5  29797  poimirlem1  31645  poimirlem2  31646  poimirlem3  31647  poimirlem4  31648  poimirlem5  31649  poimirlem6  31650  poimirlem7  31651  poimirlem11  31655  poimirlem12  31656  poimirlem16  31660  poimirlem17  31661  poimirlem19  31663  poimirlem20  31664  poimirlem22  31666  poimirlem23  31667  poimirlem24  31668  poimirlem25  31669  poimirlem28  31672  poimirlem29  31673  poimirlem31  31675  poimirlem32  31676  poimir  31677  broucube  31678  mblfinlem2  31682  mblfinlem3  31683  ismblfin  31685  itg2addnclem  31697  itg2addnclem3  31699  itg2addnc  31700  ftc1anclem3  31723  ftc1anclem5  31725  ftc1anclem7  31727  ftc1anclem8  31728  ftc1anc  31729  dvacos  31733  prdsbnd  31829  heiborlem10  31856  renegclALT  32244  diophrw  35310  monotoddzzfi  35500  zindbi  35504  mncn0  35708  aaitgo  35731  flcidc  35743  dfrcl4  35911  fvrcllb0d  35928  fvrcllb0da  35929  iunrelexp0  35937  corclrcl  35942  relexp0idm  35950  dfrtrcl4  35973  corcltrcl  35974  cotrclrcl  35977  ofsubid  36314  lhe4.4ex1a  36319  dvsconst  36320  dvconstbi  36324  binomcxplemnn0  36339  binomcxplemdvbinom  36343  binomcxplemnotnn0  36346  n0p  37020  climrec  37257  dvnmptdivc  37386  dvnmul  37391  stoweidlem55  37489  fourierdlem62  37604  fourierdlem104  37646  fouriersw  37667  el1fzopredsuc  38125  usgra2adedglem1  38439  zlmodzxzel  38909  zlmodzxz0  38910  zlmodzxzscm  38911  zlmodzxzadd  38912  zlmodzxznm  39063  zlmodzxzldeplem  39064  zlmodzxzldeplem2  39067  blen0  39157  nn0sumshdiglemB  39205  ex-gt  39222  ex-gte  39223  aacllem  39314
  Copyright terms: Public domain W3C validator