Theorem snid 4606

Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 31-Dec-1993.)

Hypothesis

Ref	Expression
snid.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
snid	⊢ 𝐴 ∈ {𝐴}

Proof of Theorem snid

Step	Hyp	Ref	Expression
1		snid.1	. 2 ⊢ 𝐴 ∈ V
2		snidb 4605	. 2 ⊢ (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴})
3	1, 2	mpbi 230	1 ⊢ 𝐴 ∈ {𝐴}

Syntax hints:   ∈ wcel 2114  Vcvv 3429  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-sn 4568

This theorem is referenced by:  vsnid  4607  rabsnt  4675  sseliALT  5244  0sn0ep  5535  opthprc  5695  dmsnsnsn  6184  snsn0non  6449  fvrn0  6868  fsn  7088  fsn2  7089  fnsnbOLD  7121  fmptsng  7123  fmptsnd  7124  fvsng  7135  ovima0  7546  brtpos0  8183  tfrlem11  8327  mapsncnv  8841  0elixp  8877  domunsncan  9015  enfixsn  9024  infeq5i  9557  tc2  9661  djulcl  9834  djurcl  9835  djulf1o  9836  djuun  9850  isfin4p1  10237  fin1a2lem12  10333  dcomex  10369  axdc3lem4  10375  zornn0g  10427  axpowndlem3  10522  canthp1lem2  10576  elreal2  11055  xrinfmss  13262  fseq1p1m1  13552  1exp  14053  wrdexb  14487  divalgmod  16375  0bits  16408  lcmfunsnlem2  16609  0ram  16991  setsid  17177  imasvscafn  17501  imasvscaval  17502  gsumval2  18654  0subm  18785  gsumz  18804  smndex1mnd  18881  smndex1id  18882  mulgfval  19045  psgnsn  19495  psgnprfval2  19498  c0snmhm  20443  pzriprnglem4  21464  pzriprnglem5  21465  pzriprnglem7  21467  pzriprnglem9  21469  pzriprnglem13  21473  pzriprnglem14  21474  pzriprng1ALT  21476  mat0dimscm  22434  mat0scmat  22503  mvmumamul1  22519  m1detdiag  22562  pmatcoe1fsupp  22666  d0mat2pmat  22703  pmatcollpw3fi1lem1  22751  pmatcollpw3fi1lem2  22752  chpmat0d  22799  dfac14  23583  filconn  23848  uffix  23886  cnextfvval  24030  cnextcn  24032  ust0  24185  bndth  24925  ehl1eudis  25387  minveclem4a  25397  dvef  25947  tdeglem2  26026  mdegcl  26034  aalioulem2  26299  cxplogb  26750  xrlimcnp  26932  gausslemma2dlem4  27332  cofcutr  27916  cofcutrtime  27919  addsproplem4  27964  addsproplem5  27965  addsproplem6  27966  addsuniflem  27993  negsproplem4  28023  negsproplem5  28024  negsproplem6  28025  mulsproplem12  28119  sltmuls1  28139  sltmuls2  28140  mulsuniflem  28141  precsexlem11  28209  twocut  28415  pw2cut2  28454  axlowdimlem8  29018  axlowdimlem11  29021  upgr1e  29182  uspgr1e  29313  wlkl1loop  29706  wlk1walk  29707  wlk2v2elem1  30225  frgrncvvdeqlem7  30375  hsn0elch  31319  rabsnel  32570  aciunf1lem  32735  gsumwrd2dccatlem  33138  cyc2fv1  33182  1arithidom  33597  ply1dg1rtn0  33641  vieta  33724  lvecdim0  33751  lvecendof1f1o  33777  repr0  34755  bnj97  35008  bnj553  35040  bnj966  35086  bnj1442  35191  fineqvinfep  35269  subfacp1lem2a  35362  subfacp1lem5  35366  cvmliftlem4  35470  fmla0xp  35565  prv1n  35613  bj-0eltag  37285  poimirlem3  37944  poimirlem9  37950  poimirlem31  37972  poimirlem32  37973  prdsbnd  38114  heiborlem3  38134  grposnOLD  38203  grpokerinj  38214  0idl  38346  0rngo  38348  sticksstones11  42595  0prjspnlem  43056  0prjspnrel  43060  fvilbdRP  44117  frege54cor1c  44342  binomcxplemnotnn0  44783  snsslVD  45255  snssl  45256  unipwrVD  45258  unipwr  45259  sucidALTVD  45296  sucidALT  45297  sucidVD  45298  unisnALT  45352  nregmodel  45444  eliuniincex  45539  cnrefiisplem  46257  0cnf  46305  qndenserrnbl  46723  nnfoctbdjlem  46883  isomenndlem  46958  hoidmvlelem2  47024  hoiqssbl  47053  tannpoly  47338  sinnpoly  47339  funressnfv  47491  el1fzopredsuc  47774  setsidel  47836  sbgoldbo  48263  lincval0  48891  lcoel0  48904  1arympt1  49114  discsubc  49539  setc1onsubc  50077  initocmd  50144