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

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

Proof of Theorem c0ex
StepHypRef Expression
1 0cn 10070 . 2 0 ∈ ℂ
21elexi 3244 1 0 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  Vcvv 3231  cc 9972  0cc0 9974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-mulcl 10036  ax-i2m1 10042
This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1526  df-ex 1745  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233
This theorem is referenced by:  ofsubeq0  11055  ofsubge0  11057  elnn0  11332  un0mulcl  11365  frnnn0supp  11387  frnnn0fsupp  11388  nn0ssz  11436  nn0ind-raph  11515  xaddval  12092  xmulval  12094  ser0f  12894  facnn  13102  fac0  13103  bcval  13131  prhash2ex  13225  wrdexb  13348  s1rn  13415  eqs1  13429  repsw1  13576  cshw1  13614  s1co  13625  funcnvs2  13704  funcnvs3  13705  funcnvs4  13706  wrdlen2i  13732  wrd2pr2op  13733  wrd3tpop  13737  wwlktovf1  13746  wrdl3s3  13751  sgnval  13872  iserge0  14435  sum0  14496  sumz  14497  fsumss  14500  fsumser  14505  isumless  14621  geomulcvg  14651  rpnnen2lem1  14987  ruclem4  15007  ruclem8  15010  ruclem11  15013  0bits  15208  gcdval  15265  lcmval  15352  lcmfpr  15387  lcmfunsnlem2  15400  prmreclem2  15668  prmreclem5  15671  vdwapun  15725  mgmnsgrpex  17465  odval  17999  odf  18002  gexval  18039  telgsumfz0  18435  telgsum  18437  srgbinom  18591  abvtrivd  18888  snifpsrbag  19414  psrbaglesupp  19416  psrbagaddcl  19418  psrbaglefi  19420  mplcoe5  19516  mplbas2  19518  ltbwe  19520  psrbag0  19542  psrbagev1  19558  cply1coe0bi  19718  m2cpminvid2lem  20607  pmatcollpw3fi1lem1  20639  pmatcollpw3fi1lem2  20640  pmatcollpw3fi1  20641  idpm2idmp  20654  prdsdsf  22219  prdsxmetlem  22220  prdsmet  22222  imasdsf1olem  22225  prdsbl  22343  xrge0gsumle  22683  xrge0tsms  22684  xrhmeo  22792  pcopt  22868  pcopt2  22869  pcoass  22870  rrxcph  23226  ovoliunnul  23321  ovolicc1  23330  vitalilem5  23426  mbfpos  23463  0pval  23483  0pledm  23485  i1f1lem  23501  i1f1  23502  itg11  23503  itg1addlem3  23510  itg1addlem4  23511  i1fres  23517  itg1climres  23526  mbfi1fseqlem4  23530  mbfi1fseqlem6  23532  mbfi1flimlem  23534  mbfi1flim  23535  xrge0f  23543  itg2ge0  23547  itg2uba  23555  itg2splitlem  23560  itg2monolem1  23562  itg2gt0  23572  itg2cnlem1  23573  ibl0  23598  iblcnlem1  23599  i1fibl  23619  itgeqa  23625  itgcn  23654  dvcmul  23752  dvcmulf  23753  dvexp3  23786  rolle  23798  dveq0  23808  dv11cn  23809  tdeglem4  23865  elply2  23997  elplyd  24003  ply1term  24005  ply0  24009  plyeq0  24012  plypf1  24013  plymullem  24017  dgrlt  24067  plymul0or  24081  dvply1  24084  plydivlem4  24096  elqaalem2  24120  iaa  24125  aareccl  24126  aannenlem2  24129  tayl0  24161  taylpfval  24164  dvtaylp  24169  pserdvlem2  24227  abelthlem9  24239  logtayl  24451  cxplogb  24569  leibpilem2  24713  leibpi  24714  jensenlem2  24759  jensen  24760  amgmlem  24761  amgm  24762  igamval  24818  vmaval  24884  vmaf  24890  muval  24903  dchrelbas2  25007  dchrinvcl  25023  dchrptlem2  25035  lgseisenlem4  25148  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  padicval  25351  padicabv  25364  ostth1  25367  axlowdimlem8  25874  axlowdimlem9  25875  axlowdimlem10  25876  axlowdimlem11  25877  axlowdimlem12  25878  axlowdimlem13  25879  axlowdimlem17  25883  uspgr1ewop  26185  usgr2v1e2w  26189  umgr2v2eedg  26476  umgr2v2e  26477  umgr2v2evd2  26479  wlkl1loop  26590  2wlklem  26619  usgr2trlncl  26712  2wlkdlem4  26893  2wlkdlem5  26894  2pthdlem1  26895  2wlkdlem10  26900  umgrwwlks2on  26923  rusgrnumwwlkl1  26935  clwwlkn2  27007  0spth  27104  1wlkdlem4  27118  wlk2v2elem1  27133  3wlkdlem4  27140  3wlkdlem5  27141  3pthdlem1  27142  3wlkdlem10  27147  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  eulerpathpr  27218  konigsberglem4  27233  konigsberglem5  27234  occllem  28290  0cnfn  28967  0lnfn  28972  nmfn0  28974  nmcexi  29013  nlelchi  29048  fprodex01  29699  sgnsval  29856  sgnsf  29857  xrge0tsmsd  29913  xrge0iif1  30112  xrge0mulc1cn  30115  gsumesum  30249  esumpfinval  30265  esumpfinvalf  30266  ddeval1  30425  ddeval0  30426  ddemeas  30427  eulerpartlemt  30561  coinfliprv  30672  sgncl  30728  plymul02  30751  plymulx  30753  signsw0glem  30758  signsw0g  30761  signswmnd  30762  signswrid  30763  signstfvn  30774  prodfzo03  30809  circlevma  30848  circlemethhgt  30849  hgt750lemg  30860  hgt750lemb  30862  hgt750lema  30863  hgt750leme  30864  tgoldbachgtde  30866  tgoldbachgt  30869  cvmliftlem4  31396  cvmliftlem5  31397  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem11  33550  poimirlem12  33551  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem22  33561  poimirlem23  33562  poimirlem24  33563  poimirlem25  33564  poimirlem28  33567  poimirlem29  33568  poimirlem31  33570  poimirlem32  33571  poimir  33572  broucube  33573  mblfinlem2  33577  mblfinlem3  33578  ismblfin  33580  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  ftc1anclem3  33617  ftc1anclem5  33619  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  dvacos  33627  prdsbnd  33722  heiborlem10  33749  renegclALT  34567  diophrw  37639  monotoddzzfi  37824  zindbi  37828  mncn0  38026  aaitgo  38049  flcidc  38061  dfrcl4  38285  fvrcllb0d  38302  fvrcllb0da  38303  iunrelexp0  38311  corclrcl  38316  relexp0idm  38324  dfrtrcl4  38347  corcltrcl  38348  cotrclrcl  38351  ofsubid  38840  lhe4.4ex1a  38845  dvsconst  38846  dvconstbi  38850  binomcxplemnn0  38865  binomcxplemdvbinom  38869  binomcxplemnotnn0  38872  n0p  39523  climrec  40153  limsup10exlem  40322  dvnmptdivc  40471  dvnmul  40476  stoweidlem55  40590  fourierdlem62  40703  fourierdlem104  40745  fouriersw  40766  rrxbasefi  40821  ovnval2  41080  hoidmvval  41112  hoidmvlelem1  41130  fun2dmnopgexmpl  41626  el1fzopredsuc  41660  zlmodzxzel  42458  zlmodzxz0  42459  zlmodzxzscm  42460  zlmodzxzadd  42461  zlmodzxznm  42611  zlmodzxzldeplem  42612  zlmodzxzldeplem2  42615  blen0  42691  nn0sumshdiglemB  42739  ex-gt  42797  ex-gte  42798  aacllem  42875
  Copyright terms: Public domain W3C validator