Theorem c0ex 11227

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459  ℂcc 11125  0cc0 11127

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-i2m1 11195

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461

This theorem is referenced by:  ofsubeq0  12235  ofsubge0  12237  elnn0  12501  un0mulcl  12533  fcdmnn0supp  12556  fcdmnn0fsupp  12557  fcdmnn0suppg  12558  fcdmnn0fsuppg  12559  nn0ssz  12609  nn0ind-raph  12691  xaddval  13237  xmulval  13239  ser0f  14071  facnn  14291  fac0  14292  bcval  14320  prhash2ex  14415  wrdexb  14541  s1rn  14615  eqs1  14628  repsw1  14799  cshw1  14838  s1co  14850  funcnvs2  14930  funcnvs3  14931  funcnvs4  14932  wrdlen2i  14959  wrd2pr2op  14960  wrd3tpop  14965  wwlktovf1  14974  wrdl3s3  14979  sgnval  15105  iserge0  15675  sum0  15735  sumz  15736  fsumss  15739  fsumser  15744  isumless  15859  geomulcvg  15890  rpnnen2lem1  16230  ruclem4  16250  ruclem8  16253  ruclem11  16256  0bits  16456  gcdval  16513  lcmval  16609  lcmfpr  16644  lcmfunsnlem2  16657  prmreclem2  16935  prmreclem5  16938  vdwapun  16992  smndex1n0mnd  18888  mgmnsgrpex  18907  odval  19513  odf  19516  gexval  19557  telgsumfz0  19971  telgsum  19973  srgbinom  20189  abvtrivd  20790  pzriprnglem4  21443  pzriprnglem5  21444  pzriprnglem7  21446  pzriprnglem9  21448  pzriprnglem10  21449  snifpsrbag  21878  psrbaglesupp  21880  psrbaglefi  21884  mplcoe5  21996  mplbas2  21998  ltbwe  22000  psrbag0  22018  psrbagev1  22033  mhpmulcl  22085  psdmplcl  22098  psdmvr  22105  cply1coe0bi  22238  m2cpminvid2lem  22690  pmatcollpw3fi1lem1  22722  pmatcollpw3fi1lem2  22723  pmatcollpw3fi1  22724  idpm2idmp  22737  prdsdsf  24304  prdsxmetlem  24305  prdsmet  24307  imasdsf1olem  24310  prdsbl  24428  xrge0gsumle  24771  xrge0tsms  24772  xrhmeo  24893  pcopt  24971  pcopt2  24972  pcoass  24973  rrxcph  25342  rrx0el  25348  rrxbasefi  25360  ovoliunnul  25458  ovolicc1  25467  vitalilem5  25563  mbfpos  25602  0pval  25622  0pledm  25624  i1f1lem  25640  i1f1  25641  itg11  25642  itg1addlem3  25649  itg1addlem4  25650  i1fres  25656  itg1climres  25665  mbfi1fseqlem4  25669  mbfi1fseqlem6  25671  mbfi1flimlem  25673  mbfi1flim  25674  xrge0f  25682  itg2ge0  25686  itg2uba  25694  itg2splitlem  25699  itg2monolem1  25701  itg2gt0  25711  itg2cnlem1  25712  ibl0  25738  iblcnlem1  25739  i1fibl  25759  itgeqa  25765  itgcn  25796  dvcmul  25897  dvcmulf  25898  dvexp3  25932  dvef  25934  rolle  25944  dveq0  25955  dv11cn  25956  tdeglem4  26015  elply2  26151  elplyd  26157  ply1term  26159  ply0  26163  plyeq0  26166  plypf1  26167  plymullem  26171  dgrlt  26222  plymul0or  26238  dvply1  26241  plydivlem4  26254  elqaalem2  26278  iaa  26283  aareccl  26284  aannenlem2  26287  tayl0  26319  taylpfval  26322  dvtaylp  26328  pserdvlem2  26388  abelthlem9  26400  logtayl  26619  cxplogb  26746  leibpilem2  26901  leibpi  26902  jensenlem2  26948  jensen  26949  amgmlem  26950  amgm  26951  igamval  27007  vmaval  27073  vmaf  27079  muval  27092  dchrelbas2  27198  dchrinvcl  27214  dchrptlem2  27226  lgseisenlem4  27339  addsqnreup  27404  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  padicval  27578  padicabv  27591  ostth1  27594  axlowdimlem8  28874  axlowdimlem9  28875  axlowdimlem10  28876  axlowdimlem11  28877  axlowdimlem12  28878  axlowdimlem13  28879  axlowdimlem17  28883  uspgr1ewop  29173  usgr2v1e2w  29177  umgr2v2eedg  29450  umgr2v2e  29451  umgr2v2evd2  29453  wlkl1loop  29564  2wlklem  29593  usgr2trlncl  29688  2wlkdlem4  29856  2wlkdlem5  29857  2pthdlem1  29858  2wlkdlem10  29863  umgrwwlks2on  29885  rusgrnumwwlkl1  29896  clwwlkn2  29971  0spth  30053  1wlkdlem4  30067  wlk2v2elem1  30082  3wlkdlem4  30089  3wlkdlem5  30090  3pthdlem1  30091  3wlkdlem10  30096  upgr3v3e3cycl  30107  upgr4cycl4dv4e  30112  eulerpathpr  30167  konigsberglem4  30182  konigsberglem5  30183  wlkl0  30294  occllem  31230  0cnfn  31907  0lnfn  31912  nmfn0  31914  nmcexi  31953  nlelchi  31988  fprodex01  32750  sgncl  32756  indsupp  32790  s2rnOLD  32865  s3rnOLD  32867  xrge0tsmsd  33002  cyc2fv1  33078  cyc3fv1  33094  cyc3evpm  33107  sgnsval  33118  sgnsf  33119  elrgspnlem1  33183  elrgspnlem4  33186  constr01  33722  constrss  33723  constrconj  33725  constrextdg2lem  33728  nn0constr  33741  xrge0iif1  33915  xrge0mulc1cn  33918  gsumesum  34036  esumpfinval  34052  esumpfinvalf  34053  ddeval1  34211  ddeval0  34212  ddemeas  34213  eulerpartlemt  34349  coinfliprv  34461  plymul02  34524  plymulx  34526  signsw0glem  34531  signsw0g  34534  signswmnd  34535  signswrid  34536  prodfzo03  34581  circlevma  34620  circlemethhgt  34621  hgt750lemg  34632  hgt750lemb  34634  hgt750lema  34635  hgt750leme  34636  tgoldbachgtde  34638  tgoldbachgt  34641  cvmliftlem4  35256  cvmliftlem5  35257  poimirlem1  37591  poimirlem2  37592  poimirlem3  37593  poimirlem4  37594  poimirlem5  37595  poimirlem6  37596  poimirlem7  37597  poimirlem11  37601  poimirlem12  37602  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem22  37612  poimirlem23  37613  poimirlem24  37614  poimirlem25  37615  poimirlem28  37618  poimirlem29  37619  poimirlem31  37621  poimirlem32  37622  poimir  37623  broucube  37624  mblfinlem2  37628  mblfinlem3  37629  ismblfin  37631  itg2addnclem  37641  itg2addnclem3  37643  itg2addnc  37644  ftc1anclem3  37665  ftc1anclem5  37667  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  dvacos  37675  prdsbnd  37763  heiborlem10  37790  renegclALT  38927  aks4d1p1p4  42030  aks6d1c7lem1  42139  0prjspnlem  42593  0prjspnrel  42597  diophrw  42729  monotoddzzfi  42913  zindbi  42917  mncn0  43110  aaitgo  43133  flcidc  43141  dfrcl4  43647  fvrcllb0d  43664  fvrcllb0da  43665  iunrelexp0  43673  corclrcl  43678  relexp0idm  43686  dfrtrcl4  43709  corcltrcl  43710  cotrclrcl  43713  ofsubid  44296  lhe4.4ex1a  44301  dvsconst  44302  dvconstbi  44306  binomcxplemnn0  44321  binomcxplemdvbinom  44325  binomcxplemnotnn0  44328  n0p  45017  climrec  45580  limsup10exlem  45749  dvnmptdivc  45915  dvnmul  45920  stoweidlem55  46032  fourierdlem62  46145  fourierdlem104  46187  fouriersw  46208  ovnval2  46522  hoidmvval  46554  tworepnotupword  46863  lambert0  46867  fun2dmnopgexmpl  47261  el1fzopredsuc  47302  cycl3grtrilem  47906  stgrusgra  47919  stgr1  47921  stgrnbgr0  47924  isubgr3stgrlem3  47928  isubgr3stgrlem7  47932  usgrexmpl1lem  47973  usgrexmpl1tri  47977  usgrexmpl2lem  47978  usgrexmpl2nb0  47983  usgrexmpl2nb1  47984  usgrexmpl2nb2  47985  usgrexmpl2nb3  47986  usgrexmpl2nb4  47987  usgrexmpl2nb5  47988  usgrexmpl2trifr  47989  gpgiedgdmellem  47998  gpgvtx0  48005  opgpgvtx  48007  gpgedgvtx0  48013  gpgvtxedg0  48015  gpgvtxedg1  48016  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem3  48023  gpg3nbgrvtx0  48026  gpg3nbgrvtx0ALT  48027  gpg3nbgrvtx1  48028  gpgcubic  48029  gpg5nbgr3star  48031  gpg3kgrtriex  48039  gpgprismgr4cycllem2  48043  gpgprismgr4cycllem3  48044  gpgprismgr4cycllem7  48048  gpgprismgr4cycllem9  48050  nn0mnd  48102  zlmodzxzel  48278  zlmodzxz0  48279  zlmodzxzscm  48280  zlmodzxzadd  48281  zlmodzxznm  48421  zlmodzxzldeplem  48422  zlmodzxzldeplem2  48425  blen0  48500  nn0sumshdiglemB  48548  fv1arycl  48565  1arympt1  48566  1arympt1fv  48567  1arymaptf1  48570  1arymaptfo  48571  fv2arycl  48576  2arympt  48577  2arymptfv  48578  2arymaptf1  48581  2arymaptfo  48582  ehl2eudisval0  48653  2sphere0  48678  line2ylem  48679  line2  48680  line2x  48682  line2y  48683  ex-gt  49540  ex-gte  49541  aacllem  49613