Theorem c0ex 11175

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 11173	. 2 ⊢ 0 ∈ ℂ
2	1	elexi 3473	1 ⊢ 0 ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3450  ℂcc 11073  0cc0 11075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-i2m1 11143

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452

This theorem is referenced by:  ofsubeq0  12190  ofsubge0  12192  elnn0  12451  un0mulcl  12483  fcdmnn0supp  12506  fcdmnn0fsupp  12507  fcdmnn0suppg  12508  fcdmnn0fsuppg  12509  nn0ssz  12559  nn0ind-raph  12641  xaddval  13190  xmulval  13192  ser0f  14027  facnn  14247  fac0  14248  bcval  14276  prhash2ex  14371  wrdexb  14497  s1rn  14571  eqs1  14584  repsw1  14755  cshw1  14794  s1co  14806  funcnvs2  14886  funcnvs3  14887  funcnvs4  14888  wrdlen2i  14915  wrd2pr2op  14916  wrd3tpop  14921  wwlktovf1  14930  wrdl3s3  14935  sgnval  15061  iserge0  15634  sum0  15694  sumz  15695  fsumss  15698  fsumser  15703  isumless  15818  geomulcvg  15849  rpnnen2lem1  16189  ruclem4  16209  ruclem8  16212  ruclem11  16215  0bits  16416  gcdval  16473  lcmval  16569  lcmfpr  16604  lcmfunsnlem2  16617  prmreclem2  16895  prmreclem5  16898  vdwapun  16952  smndex1n0mnd  18846  mgmnsgrpex  18865  odval  19471  odf  19474  gexval  19515  telgsumfz0  19929  telgsum  19931  srgbinom  20147  abvtrivd  20748  pzriprnglem4  21401  pzriprnglem5  21402  pzriprnglem7  21404  pzriprnglem9  21406  pzriprnglem10  21407  snifpsrbag  21836  psrbaglesupp  21838  psrbaglefi  21842  mplcoe5  21954  mplbas2  21956  ltbwe  21958  psrbag0  21976  psrbagev1  21991  mhpmulcl  22043  psdmplcl  22056  psdmvr  22063  cply1coe0bi  22196  m2cpminvid2lem  22648  pmatcollpw3fi1lem1  22680  pmatcollpw3fi1lem2  22681  pmatcollpw3fi1  22682  idpm2idmp  22695  prdsdsf  24262  prdsxmetlem  24263  prdsmet  24265  imasdsf1olem  24268  prdsbl  24386  xrge0gsumle  24729  xrge0tsms  24730  xrhmeo  24851  pcopt  24929  pcopt2  24930  pcoass  24931  rrxcph  25299  rrx0el  25305  rrxbasefi  25317  ovoliunnul  25415  ovolicc1  25424  vitalilem5  25520  mbfpos  25559  0pval  25579  0pledm  25581  i1f1lem  25597  i1f1  25598  itg11  25599  itg1addlem3  25606  itg1addlem4  25607  i1fres  25613  itg1climres  25622  mbfi1fseqlem4  25626  mbfi1fseqlem6  25628  mbfi1flimlem  25630  mbfi1flim  25631  xrge0f  25639  itg2ge0  25643  itg2uba  25651  itg2splitlem  25656  itg2monolem1  25658  itg2gt0  25668  itg2cnlem1  25669  ibl0  25695  iblcnlem1  25696  i1fibl  25716  itgeqa  25722  itgcn  25753  dvcmul  25854  dvcmulf  25855  dvexp3  25889  dvef  25891  rolle  25901  dveq0  25912  dv11cn  25913  tdeglem4  25972  elply2  26108  elplyd  26114  ply1term  26116  ply0  26120  plyeq0  26123  plypf1  26124  plymullem  26128  dgrlt  26179  plymul0or  26195  dvply1  26198  plydivlem4  26211  elqaalem2  26235  iaa  26240  aareccl  26241  aannenlem2  26244  tayl0  26276  taylpfval  26279  dvtaylp  26285  pserdvlem2  26345  abelthlem9  26357  logtayl  26576  cxplogb  26703  leibpilem2  26858  leibpi  26859  jensenlem2  26905  jensen  26906  amgmlem  26907  amgm  26908  igamval  26964  vmaval  27030  vmaf  27036  muval  27049  dchrelbas2  27155  dchrinvcl  27171  dchrptlem2  27183  lgseisenlem4  27296  addsqnreup  27361  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  padicval  27535  padicabv  27548  ostth1  27551  axlowdimlem8  28883  axlowdimlem9  28884  axlowdimlem10  28885  axlowdimlem11  28886  axlowdimlem12  28887  axlowdimlem13  28888  axlowdimlem17  28892  uspgr1ewop  29182  usgr2v1e2w  29186  umgr2v2eedg  29459  umgr2v2e  29460  umgr2v2evd2  29462  wlkl1loop  29573  2wlklem  29602  usgr2trlncl  29697  2wlkdlem4  29865  2wlkdlem5  29866  2pthdlem1  29867  2wlkdlem10  29872  umgrwwlks2on  29894  rusgrnumwwlkl1  29905  clwwlkn2  29980  0spth  30062  1wlkdlem4  30076  wlk2v2elem1  30091  3wlkdlem4  30098  3wlkdlem5  30099  3pthdlem1  30100  3wlkdlem10  30105  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  eulerpathpr  30176  konigsberglem4  30191  konigsberglem5  30192  wlkl0  30303  occllem  31239  0cnfn  31916  0lnfn  31921  nmfn0  31923  nmcexi  31962  nlelchi  31997  fprodex01  32757  sgncl  32763  indsupp  32797  s2rnOLD  32872  s3rnOLD  32874  xrge0tsmsd  33009  cyc2fv1  33085  cyc3fv1  33101  cyc3evpm  33114  sgnsval  33125  sgnsf  33126  elrgspnlem1  33200  elrgspnlem4  33203  constr01  33739  constrss  33740  constrconj  33742  constrextdg2lem  33745  nn0constr  33758  xrge0iif1  33935  xrge0mulc1cn  33938  gsumesum  34056  esumpfinval  34072  esumpfinvalf  34073  ddeval1  34231  ddeval0  34232  ddemeas  34233  eulerpartlemt  34369  coinfliprv  34481  plymul02  34544  plymulx  34546  signsw0glem  34551  signsw0g  34554  signswmnd  34555  signswrid  34556  prodfzo03  34601  circlevma  34640  circlemethhgt  34641  hgt750lemg  34652  hgt750lemb  34654  hgt750lema  34655  hgt750leme  34656  tgoldbachgtde  34658  tgoldbachgt  34661  cvmliftlem4  35282  cvmliftlem5  35283  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem4  37625  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem11  37632  poimirlem12  37633  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem28  37649  poimirlem29  37650  poimirlem31  37652  poimirlem32  37653  poimir  37654  broucube  37655  mblfinlem2  37659  mblfinlem3  37660  ismblfin  37662  itg2addnclem  37672  itg2addnclem3  37674  itg2addnc  37675  ftc1anclem3  37696  ftc1anclem5  37698  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  dvacos  37706  prdsbnd  37794  heiborlem10  37821  renegclALT  38963  aks4d1p1p4  42066  aks6d1c7lem1  42175  0prjspnlem  42618  0prjspnrel  42622  diophrw  42754  monotoddzzfi  42938  zindbi  42942  mncn0  43135  aaitgo  43158  flcidc  43166  dfrcl4  43672  fvrcllb0d  43689  fvrcllb0da  43690  iunrelexp0  43698  corclrcl  43703  relexp0idm  43711  dfrtrcl4  43734  corcltrcl  43735  cotrclrcl  43738  ofsubid  44320  lhe4.4ex1a  44325  dvsconst  44326  dvconstbi  44330  binomcxplemnn0  44345  binomcxplemdvbinom  44349  binomcxplemnotnn0  44352  n0p  45046  climrec  45608  limsup10exlem  45777  dvnmptdivc  45943  dvnmul  45948  stoweidlem55  46060  fourierdlem62  46173  fourierdlem104  46215  fouriersw  46236  ovnval2  46550  hoidmvval  46582  tworepnotupword  46891  lambert0  46895  fun2dmnopgexmpl  47289  el1fzopredsuc  47330  cycl3grtrilem  47949  stgrusgra  47962  stgr1  47964  stgrnbgr0  47967  isubgr3stgrlem3  47971  isubgr3stgrlem7  47975  usgrexmpl1lem  48016  usgrexmpl1tri  48020  usgrexmpl2lem  48021  usgrexmpl2nb0  48026  usgrexmpl2nb1  48027  usgrexmpl2nb2  48028  usgrexmpl2nb3  48029  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  usgrexmpl2trifr  48032  gpgiedgdmellem  48041  gpgvtx0  48048  opgpgvtx  48050  gpgedgvtx0  48056  gpgvtxedg0  48058  gpgvtxedg1  48059  gpgedgiov  48060  gpgedg2ov  48061  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem3  48068  gpg3nbgrvtx0  48071  gpg3nbgrvtx0ALT  48072  gpg3nbgrvtx1  48073  gpgcubic  48074  gpg5nbgr3star  48076  gpg3kgrtriex  48084  gpgprismgr4cycllem2  48090  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem7  48095  gpgprismgr4cycllem9  48097  pgnioedg1  48102  pgnioedg2  48103  pgnioedg3  48104  pgnioedg4  48105  pgnioedg5  48106  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem5lem3  48116  pgnbgreunbgrlem5  48117  pgnbgreunbgrlem6  48118  nn0mnd  48171  zlmodzxzel  48347  zlmodzxz0  48348  zlmodzxzscm  48349  zlmodzxzadd  48350  zlmodzxznm  48490  zlmodzxzldeplem  48491  zlmodzxzldeplem2  48494  blen0  48565  nn0sumshdiglemB  48613  fv1arycl  48630  1arympt1  48631  1arympt1fv  48632  1arymaptf1  48635  1arymaptfo  48636  fv2arycl  48641  2arympt  48642  2arymptfv  48643  2arymaptf1  48646  2arymaptfo  48647  ehl2eudisval0  48718  2sphere0  48743  line2ylem  48744  line2  48745  line2x  48747  line2y  48748  ex-gt  49721  ex-gte  49722  aacllem  49794