Theorem c0ex 11304

Description: Zero is a set. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
c0ex	⊢ 0 ∈ V

Proof of Theorem c0ex

Step	Hyp	Ref	Expression
1		0cn 11302	. 2 ⊢ 0 ∈ ℂ
2	1	elexi 3472	1 ⊢ 0 ∈ V

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  ℂcc 11202  0cc0 11204

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-mulcl 11266  ax-i2m1 11272

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  0elpr01  11305  ofsubeq0  12321  ofsubge0  12323  elnn0  12612  un0mulcl  12644  fcdmnn0supp  12667  fcdmnn0fsupp  12668  fcdmnn0suppg  12669  fcdmnn0fsuppg  12670  nn0ssz  12720  nn0ind-raph  12803  xaddval  13357  xmulval  13359  ser0f  14202  facnn  14423  fac0  14424  bcval  14452  prhash2ex  14547  wrdexb  14674  s1rn  14750  eqs1  14765  repsw1  14939  cshw1  14978  s1co  14989  funcnvs2  15070  funcnvs3  15071  funcnvs4  15072  wrdlen2i  15099  wrd2pr2op  15100  wrd3tpop  15105  s3rex  15107  wwlktovf1  15116  wrdl3s3  15121  sgnval  15247  sgndm  15255  sgncl  15256  iserge0  15834  sum0  15893  sumz  15894  fsumss  15897  fsumser  15902  isumless  16020  geomulcvg  16051  rpnnen2lem1  16388  ruclem4  16408  ruclem8  16411  ruclem11  16414  0bits  16615  gcdval  16672  lcmval  16773  lcmfpr  16808  lcmfunsnlem2  16821  prmreclem2  17101  prmreclem5  17104  vdwapun  17158  smndex1n0mnd  19117  mgmnsgrpex  19136  odval  19754  odf  19757  gexval  19798  telgsumfz0  20212  telgsum  20214  srgbinom  20463  abvtrivd  21095  pzriprnglem4  21796  pzriprnglem5  21797  pzriprnglem7  21799  pzriprnglem9  21801  pzriprnglem10  21802  snifpsrbag  22234  psrbaglesupp  22236  psrbaglefi  22240  mplcoe5  22355  mplbas2  22357  ltbwe  22359  psrbag0  22377  psrbagev1  22392  mhpmulcl  22476  psdmplcl  22489  psdmvr  22496  cply1coe0bi  22626  m2cpminvid2lem  23078  pmatcollpw3fi1lem1  23110  pmatcollpw3fi1lem2  23111  pmatcollpw3fi1  23112  idpm2idmp  23125  prdsdsf  24692  prdsxmetlem  24693  prdsmet  24695  imasdsf1olem  24698  prdsbl  24816  xrge0gsumle  25159  xrge0tsms  25160  xrhmeo  25273  pcopt  25349  pcopt2  25350  pcoass  25351  rrxcph  25719  rrx0el  25725  rrxbasefi  25737  ehlbase  25742  ehl1eudis  25747  ehl2eudis  25749  ovoliunnul  25834  ovolicc1  25843  vitalilem5  25939  mbfpos  25978  0pval  25998  0pledm  26000  i1f1lem  26016  itg11  26018  itg1addlem3  26025  itg1addlem4  26026  i1fres  26032  itg1climres  26041  mbfi1fseqlem4  26045  mbfi1fseqlem6  26047  mbfi1flimlem  26049  mbfi1flim  26050  xrge0f  26058  itg2ge0  26062  itg2uba  26070  itg2splitlem  26075  itg2monolem1  26077  itg2gt0  26087  itg2cnlem1  26088  ibl0  26113  iblcnlem1  26114  i1fibl  26134  itgeqa  26140  itgcn  26171  dvcmul  26270  dvcmulf  26271  dvexp3  26304  dvef  26306  rolle  26316  dveq0  26326  dv11cn  26327  tdeglem4  26384  elply2  26520  elplyd  26526  ply1term  26528  ply0  26532  plyeq0  26536  plypf1  26537  plymullem  26541  dgrlt  26591  plymul0or  26605  plymul02  26607  plymulidp  26609  dvply1  26611  plydivlem4  26623  elqaalem2  26649  iaaOLD  26658  aareccl  26659  aannenlem2  26662  tayl0  26695  taylpfval  26698  dvtaylp  26703  pserdvlem2  26761  abelthlem9  26773  logtayl  26994  cxplogb  27120  leibpilem2  27275  leibpi  27276  jensenlem2  27321  jensen  27322  amgmlem  27323  amgm  27324  igamval  27380  vmaval  27446  vmaf  27452  muval  27465  dchrelbas2  27570  dchrinvcl  27586  dchrptlem2  27598  lgseisenlem4  27711  addsqnreup  27776  pntrlog2bndlem4  27913  pntrlog2bndlem5  27914  padicval  27950  padicabv  27963  ostth1  27966  elcgrabasi  29381  axlowdimlem8  29533  axlowdimlem9  29534  axlowdimlem10  29535  axlowdimlem11  29536  axlowdimlem12  29537  axlowdimlem13  29538  axlowdimlem17  29542  uspgr1ewop  29835  usgr2v1e2w  29839  umgr2v2eedg  30111  umgr2v2e  30112  umgr2v2evd2  30114  wlkl1loop  30224  2wlklem  30252  usgr2trlncl  30352  2wlkdlem4  30523  2wlkdlem5  30524  2pthdlem1  30525  2wlkdlem10  30530  usgrwwlks2on  30553  umgrwwlks2on  30554  rusgrnumwwlkl1  30566  clwwlkn2  30641  0spth  30723  1wlkdlem4  30737  wlk2v2elem1  30762  3wlkdlem4  30769  3wlkdlem5  30770  3pthdlem1  30771  3wlkdlem10  30776  upgr3v3e3cycl  30787  upgr4cycl4dv4e  30792  eulerpathpr  30847  konigsberglem4  30862  konigsberglem5  30863  wlkl0  30974  occllem  31911  0cnfn  32588  0lnfn  32593  nmfn0  32595  nmcexi  32634  nlelchi  32669  fprodex01  33463  indsupp  33481  indfsd  33482  indfsid  33483  gsummulsubdishift1  33676  gsummulsubdishift2s  33679  xrge0tsmsd  33681  cyc2fv1  33729  cyc3evpm  33758  sgnsval  33769  sgnsf  33770  elrgspnlem1  33850  elrgspnlem4  33853  gsumind  33953  0mplrim  34193  selvply1rhmlema  34197  selvply1rhmlemb  34198  selvply1rhmlem1  34199  selvply1rhmlem2  34200  selvply1rhmlem4  34202  selvply1rhm0  34205  extvfvvcl  34214  extvfvcl  34215  esplyfval0  34243  esplysply  34250  esplyind  34254  vieta  34259  constrextdg2lem  34427  xrge0iif1  34617  xrge0mulc1cn  34620  gsumesum  34738  esumpfinval  34754  esumpfinvalf  34755  ddeval1  34914  ddeval0  34915  ddemeas  34916  eulerpartlemt  35050  coinfliprv  35162  signsw0glem  35229  signsw0g  35232  signswmnd  35233  signswrid  35234  prodfzo03  35279  circlevma  35318  circlemethhgt  35319  hgt750lemg  35330  hgt750lemb  35332  hgt750lema  35333  hgt750leme  35334  tgoldbachgtde  35336  tgoldbachgt  35339  cvmliftlem4  36140  cvmliftlem5  36141  poimirlem1  38633  poimirlem2  38634  poimirlem3  38635  poimirlem4  38636  poimirlem5  38637  poimirlem6  38638  poimirlem7  38639  poimirlem11  38643  poimirlem12  38644  poimirlem16  38648  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  poimirlem22  38654  poimirlem23  38655  poimirlem24  38656  poimirlem25  38657  poimirlem28  38660  poimirlem29  38661  poimirlem31  38663  poimirlem32  38664  poimir  38665  broucube  38666  mblfinlem2  38670  mblfinlem3  38671  ismblfin  38673  itg2addnclem  38683  itg2addnclem3  38685  itg2addnc  38686  ftc1anclem3  38707  ftc1anclem5  38709  ftc1anclem7  38711  ftc1anclem8  38712  ftc1anc  38713  dvacos  38717  prdsbnd  38821  heiborlem10  38848  renegclALT  40114  aks4d1p1p4  43215  aks6d1c7lem1  43324  0prjspnlem  43756  0prjspnrel  43757  diophrw  43864  monotoddzzfi  44043  zindbi  44047  mncn0  44235  aaitgo  44258  flcidc  44266  dfrcl4  44770  iunrelexp0  44796  corclrcl  44801  relexp0idm  44809  dfrtrcl4  44832  corcltrcl  44833  cotrclrcl  44836  ofsubid  45402  lhe4.4ex1a  45407  dvsconst  45408  dvconstbi  45412  binomcxplemnn0  45427  binomcxplemdvbinom  45431  binomcxplemnotnn0  45434  n0p  46156  climrec  46709  limsup10exlem  46876  dvnmptdivc  47042  dvnmul  47047  stoweidlem55  47159  fourierdlem62  47272  fourierdlem104  47314  fouriersw  47335  ovnval2  47649  hoidmvval  47681  lambert0  48031  tannpoly  48034  sinnpoly  48035  fun2dmnopgexmpl  48448  el1fzopredsuc  48490  cycl3grtrilem  49138  stgrusgra  49151  stgrnbgr0  49156  isubgr3stgrlem3  49160  isubgr3stgrlem7  49164  usgrexmpl1lem  49213  usgrexmpl1tri  49217  usgrexmpl2lem  49218  usgrexmpl2nb0  49223  usgrexmpl2nb1  49224  usgrexmpl2nb2  49225  usgrexmpl2nb3  49226  usgrexmpl2nb4  49227  usgrexmpl2nb5  49228  usgrexmpl2trifr  49229  opgpgvtx  49247  gpgedgvtx0  49253  gpgvtxedg0  49255  gpgvtxedg1  49256  gpgedgiov  49257  gpgedg2ov  49258  gpg5nbgrvtx03starlem1  49260  gpg5nbgrvtx03starlem2  49261  gpg5nbgrvtx03starlem3  49262  gpg5nbgrvtx13starlem1  49263  gpg5nbgrvtx13starlem3  49265  gpg3nbgrvtx0  49268  gpg3nbgrvtx0ALT  49269  gpg3nbgrvtx1  49270  gpgcubic  49271  gpg5nbgr3star  49273  gpg3kgrtriex  49281  gpgprismgr4cycllem2  49288  gpgprismgr4cycllem7  49293  pgnioedg1  49300  pgnioedg2  49301  pgnioedg3  49302  pgnioedg4  49303  pgnioedg5  49304  pgnbgreunbgrlem1  49305  pgnbgreunbgrlem2lem1  49306  pgnbgreunbgrlem2lem2  49307  pgnbgreunbgrlem2lem3  49308  pgnbgreunbgrlem3  49310  pgnbgreunbgrlem5lem3  49314  pgnbgreunbgrlem5  49315  pgnbgreunbgrlem6  49316  gpg5edgnedg  49322  nn0mnd  49370  zlmodzxzel  49561  zlmodzxz0  49562  zlmodzxzscm  49563  zlmodzxzadd  49564  zlmodzxznm  49703  zlmodzxzldeplem  49704  zlmodzxzldeplem2  49707  blen0  49778  nn0sumshdiglemB  49826  fv1arycl  49843  1arympt1  49844  1arympt1fv  49845  1arymaptf1  49848  1arymaptfo  49849  fv2arycl  49854  2arymptfv  49856  2arymaptf1  49859  2arymaptfo  49860  rrx2pnecoorneor  49922  ehl2eudisval0  49932  rrx2line  49946  rrx2linest  49948  2sphere0  49956  line2ylem  49957  line2  49958  ex-gt  50990  ex-gte  50991  aacllem  51108