Theorem snid 4601

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 4600	. 2 ⊢ (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴})
3	1, 2	mpbi 232	1 ⊢ 𝐴 ∈ {𝐴}

Syntax hints:   ∈ wcel 2114  Vcvv 3494  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-sn 4568

This theorem is referenced by:  vsnid  4602  rabsnt  4667  sseliALT  5213  elALT  5335  intid  5350  0sn0ep  5470  opthprc  5616  dmsnsnsn  6077  snsn0non  6309  fvrn0  6698  fsn  6897  fsn2  6898  fnsnb  6928  fmptsng  6930  fmptsnd  6931  fvsng  6942  ovima0  7327  brtpos0  7899  tfrlem11  8024  mapsncnv  8457  0elixp  8493  domunsncan  8617  enfixsn  8626  infeq5i  9099  tc2  9184  djulcl  9339  djurcl  9340  djulf1o  9341  djuun  9355  isfin4p1  9737  fin1a2lem12  9833  dcomex  9869  axdc3lem4  9875  zornn0g  9927  axpowndlem3  10021  canthp1lem2  10075  elreal2  10554  xrinfmss  12704  fseq1p1m1  12982  1exp  13459  wrdexb  13874  divalgmod  15757  0bits  15788  lcmfunsnlem2  15984  0ram  16356  setsid  16538  imasvscafn  16810  imasvscaval  16811  gsumval2  17896  0subm  17982  gsumz  18000  smndex1mnd  18075  smndex1id  18076  mulgfval  18226  psgnsn  18648  psgnprfval2  18651  mat0dimscm  21078  mat0scmat  21147  mvmumamul1  21163  m1detdiag  21206  pmatcoe1fsupp  21309  d0mat2pmat  21346  pmatcollpw3fi1lem1  21394  pmatcollpw3fi1lem2  21395  chpmat0d  21442  dfac14  22226  filconn  22491  uffix  22529  cnextfvval  22673  cnextcn  22675  ust0  22828  bndth  23562  ehl1eudis  24023  minveclem4a  24033  dvef  24577  tdeglem2  24655  mdegcl  24663  aalioulem2  24922  cxplogb  25364  xrlimcnp  25546  gausslemma2dlem4  25945  axlowdimlem8  26735  axlowdimlem11  26738  upgr1e  26898  uspgr1e  27026  wlkl1loop  27419  wlk1walk  27420  wlk2v2elem1  27934  frgrncvvdeqlem7  28084  hsn0elch  29025  rabsnel  30263  aciunf1lem  30407  cyc2fv1  30763  lvecdim0  31005  repr0  31882  bnj97  32138  bnj553  32170  bnj966  32216  bnj1442  32321  subfacp1lem2a  32427  subfacp1lem5  32431  cvmliftlem4  32535  fmla0xp  32630  prv1n  32678  bj-0eltag  34293  poimirlem3  34910  poimirlem9  34916  poimirlem31  34938  poimirlem32  34939  prdsbnd  35086  heiborlem3  35106  grposnOLD  35175  grpokerinj  35186  0idl  35318  0rngo  35320  0prjspnlem  39288  0prjspnrel  39289  fvilbdRP  40055  frege54cor1c  40281  binomcxplemnotnn0  40708  snsslVD  41183  snssl  41184  unipwrVD  41186  unipwr  41187  sucidALTVD  41224  sucidALT  41225  sucidVD  41226  unisnALT  41280  eliuniincex  41395  cnrefiisplem  42130  0cnf  42180  dvmptfprod  42250  qndenserrnbl  42600  nnfoctbdjlem  42757  isomenndlem  42832  hoidmvlelem2  42898  hoiqssbl  42927  funressnfv  43298  el1fzopredsuc  43545  setsidel  43556  sbgoldbo  43972  c0snmhm  44206  lincval0  44490  lcoel0  44503