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

Theorem c0ex 9890
Description: 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
c0ex 0 ∈ V

Proof of Theorem c0ex
StepHypRef Expression
1 0cn 9888 . 2 0 ∈ ℂ
21elexi 3185 1 0 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  Vcvv 3172  cc 9790  0cc0 9792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033  ax-ext 2589  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-mulcl 9854  ax-i2m1 9860
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-v 3174
This theorem is referenced by:  ofsubeq0  10864  ofsubge0  10866  elnn0  11141  un0mulcl  11174  frnnn0supp  11196  frnnn0fsupp  11197  nn0ssz  11231  nn0ind-raph  11309  xaddval  11887  xmulval  11889  ser0f  12671  facnn  12879  fac0  12880  bcval  12908  prhash2ex  13000  wrdexb  13117  s1rn  13178  eqs1  13191  repsw1  13327  cshw1  13365  s1co  13376  funcnvs2  13454  funcnvs3  13455  funcnvs4  13456  wrdlen2i  13480  wrd2pr2op  13481  wrd3tpop  13485  wwlktovf1  13494  wrdl3s3  13499  sgnval  13622  iserge0  14185  sum0  14245  sumz  14246  fsumss  14249  fsumser  14254  isumless  14362  geomulcvg  14392  rpnnen2lem1  14728  ruclem4  14748  ruclem8  14751  ruclem11  14754  0bits  14945  gcdval  15002  lcmval  15089  lcmfpr  15124  lcmfunsnlem2  15137  prmreclem2  15405  prmreclem5  15408  vdwapun  15462  mgmnsgrpex  17187  odval  17722  odf  17725  gexval  17762  telgsumfz0  18158  telgsum  18160  srgbinom  18314  abvtrivd  18609  snifpsrbag  19133  psrbaglesupp  19135  psrbagaddcl  19137  psrbaglefi  19139  mplcoe5  19235  mplbas2  19237  ltbwe  19239  psrbag0  19261  psrbagev1  19277  cply1coe0bi  19437  m2cpminvid2lem  20320  pmatcollpw3fi1lem1  20352  pmatcollpw3fi1lem2  20353  pmatcollpw3fi1  20354  idpm2idmp  20367  prdsdsf  21923  prdsxmetlem  21924  prdsmet  21926  imasdsf1olem  21929  prdsbl  22047  xrge0gsumle  22376  xrge0tsms  22377  xrhmeo  22484  pcopt  22561  pcopt2  22562  pcoass  22563  rrxcph  22905  ovoliunnul  22999  ovolicc1  23008  vitalilem5  23104  mbfpos  23141  0pval  23161  0pledm  23163  i1f1lem  23179  i1f1  23180  itg11  23181  itg1addlem3  23188  itg1addlem4  23189  i1fres  23195  itg1climres  23204  mbfi1fseqlem4  23208  mbfi1fseqlem6  23210  mbfi1flimlem  23212  mbfi1flim  23213  xrge0f  23221  itg2ge0  23225  itg2uba  23233  itg2splitlem  23238  itg2monolem1  23240  itg2gt0  23250  itg2cnlem1  23251  ibl0  23276  iblcnlem1  23277  i1fibl  23297  itgeqa  23303  itgcn  23332  dvcmul  23430  dvcmulf  23431  dvexp3  23462  rolle  23474  dveq0  23484  dv11cn  23485  tdeglem4  23541  elply2  23673  elplyd  23679  ply1term  23681  ply0  23685  plyeq0  23688  plypf1  23689  plymullem  23693  dgrlt  23743  plymul0or  23757  dvply1  23760  plydivlem4  23772  elqaalem2  23796  iaa  23801  aareccl  23802  aannenlem2  23805  tayl0  23837  taylpfval  23840  dvtaylp  23845  pserdvlem2  23903  abelthlem9  23915  logtayl  24123  cxplogb  24241  leibpilem2  24385  leibpi  24386  jensenlem2  24431  jensen  24432  amgmlem  24433  amgm  24434  igamval  24490  vmaval  24556  vmaf  24562  muval  24575  dchrelbas2  24679  dchrinvcl  24695  dchrptlem2  24707  lgseisenlem4  24820  pntrlog2bndlem4  24986  pntrlog2bndlem5  24987  padicval  25023  padicabv  25036  ostth1  25039  axlowdimlem8  25547  axlowdimlem9  25548  axlowdimlem10  25549  axlowdimlem11  25550  axlowdimlem12  25551  axlowdimlem13  25552  axlowdimlem17  25556  2trllemA  25846  2trllemH  25848  2trllemE  25849  2wlklemA  25850  wlkntrllem1  25855  wlkntrllem2  25856  wlkntrllem3  25857  2wlklem  25860  0spth  25867  constr1trl  25884  1pthon  25887  2pthlem2  25892  2wlklem1  25893  2pthon  25898  2pthon3v  25900  usgra2adedgwlkonALT  25910  usgra2wlkspthlem1  25913  usgra2wlkspthlem2  25914  constr3lem2  25940  constr3lem4  25941  constr3lem5  25942  constr3trllem1  25944  constr3trllem2  25945  clwwlkn2  26069  usg2wlkonot  26176  usg2wotspth  26177  0egra0rgra  26229  rusgranumwlkl1  26240  eupath  26274  occllem  27352  0cnfn  28029  0lnfn  28034  nmfn0  28036  nmcexi  28075  nlelchi  28110  sgnsval  28865  sgnsf  28866  xrge0tsmsd  28922  xrge0iif1  29118  xrge0mulc1cn  29121  gsumesum  29254  esumpfinval  29270  esumpfinvalf  29271  ddeval1  29430  ddeval0  29431  ddemeas  29432  eulerpartlemt  29566  coinfliprv  29677  sgncl  29733  plymul02  29755  plymulx  29757  signsw0glem  29762  signsw0g  29765  signswmnd  29766  signswrid  29767  signstfvn  29778  cvmliftlem4  30330  cvmliftlem5  30331  poimirlem1  32376  poimirlem2  32377  poimirlem3  32378  poimirlem4  32379  poimirlem5  32380  poimirlem6  32381  poimirlem7  32382  poimirlem11  32386  poimirlem12  32387  poimirlem16  32391  poimirlem17  32392  poimirlem19  32394  poimirlem20  32395  poimirlem22  32397  poimirlem23  32398  poimirlem24  32399  poimirlem25  32400  poimirlem28  32403  poimirlem29  32404  poimirlem31  32406  poimirlem32  32407  poimir  32408  broucube  32409  mblfinlem2  32413  mblfinlem3  32414  ismblfin  32416  itg2addnclem  32427  itg2addnclem3  32429  itg2addnc  32430  ftc1anclem3  32453  ftc1anclem5  32455  ftc1anclem7  32457  ftc1anclem8  32458  ftc1anc  32459  dvacos  32463  prdsbnd  32558  heiborlem10  32585  renegclALT  33063  diophrw  36136  monotoddzzfi  36321  zindbi  36325  mncn0  36524  aaitgo  36547  flcidc  36559  dfrcl4  36783  fvrcllb0d  36800  fvrcllb0da  36801  iunrelexp0  36809  corclrcl  36814  relexp0idm  36822  dfrtrcl4  36845  corcltrcl  36846  cotrclrcl  36849  ofsubid  37341  lhe4.4ex1a  37346  dvsconst  37347  dvconstbi  37351  binomcxplemnn0  37366  binomcxplemdvbinom  37370  binomcxplemnotnn0  37373  n0p  38030  climrec  38467  dvnmptdivc  38625  dvnmul  38630  stoweidlem55  38745  fourierdlem62  38858  fourierdlem104  38900  fouriersw  38921  rrxbasefi  38976  ovnval2  39232  hoidmvval  39264  hoidmvlelem1  39282  el1fzopredsuc  39746  fun2dmnopgexmpl  40149  uspgr1ewop  40469  usgr2v1e2w  40473  umgr2v2eedg  40735  umgr2v2e  40736  umgr2v2evd2  40738  1wlkl1loop  40837  2Wlklem  40870  usgr2wlkneq  40957  usgr2trlncl  40961  21wlkdlem4  41130  21wlkdlem5  41131  2pthdlem1  41132  21wlkdlem10  41137  umgrwwlks2on  41156  rusgrnumwwlkl1  41167  clwwlksn2  41212  0spth-av  41289  11wlkdlem4  41302  1wlk2v2elem1  41317  31wlkdlem4  41324  31wlkdlem5  41325  3pthdlem1  41326  31wlkdlem10  41331  upgr3v3e3cycl  41342  upgr4cycl4dv4e  41347  eulerpathpr  41403  konigsberglem4  41420  konigsberglem5  41421  zlmodzxzel  41921  zlmodzxz0  41922  zlmodzxzscm  41923  zlmodzxzadd  41924  zlmodzxznm  42075  zlmodzxzldeplem  42076  zlmodzxzldeplem2  42079  blen0  42159  nn0sumshdiglemB  42207  ex-gt  42224  ex-gte  42225  aacllem  42312
  Copyright terms: Public domain W3C validator