Theorem snid 4621

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442  {csn 4582

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-sn 4583

This theorem is referenced by:  vsnid  4622  rabsnt  4690  sseliALT  5256  0sn0ep  5536  opthprc  5696  dmsnsnsn  6186  snsn0non  6451  fvrn0  6870  fsn  7090  fsn2  7091  fnsnbOLD  7122  fmptsng  7124  fmptsnd  7125  fvsng  7136  ovima0  7547  brtpos0  8185  tfrlem11  8329  mapsncnv  8843  0elixp  8879  domunsncan  9017  enfixsn  9026  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  13237  fseq1p1m1  13526  1exp  14026  wrdexb  14460  divalgmod  16345  0bits  16378  lcmfunsnlem2  16579  0ram  16960  setsid  17146  imasvscafn  17470  imasvscaval  17471  gsumval2  18623  0subm  18754  gsumz  18773  smndex1mnd  18847  smndex1id  18848  mulgfval  19011  psgnsn  19461  psgnprfval2  19464  c0snmhm  20411  pzriprnglem4  21451  pzriprnglem5  21452  pzriprnglem7  21454  pzriprnglem9  21456  pzriprnglem13  21460  pzriprnglem14  21461  pzriprng1ALT  21463  mat0dimscm  22425  mat0scmat  22494  mvmumamul1  22510  m1detdiag  22553  pmatcoe1fsupp  22657  d0mat2pmat  22694  pmatcollpw3fi1lem1  22742  pmatcollpw3fi1lem2  22743  chpmat0d  22790  dfac14  23574  filconn  23839  uffix  23877  cnextfvval  24021  cnextcn  24023  ust0  24176  bndth  24925  ehl1eudis  25388  minveclem4a  25398  dvef  25952  tdeglem2  26034  mdegcl  26042  aalioulem2  26309  cxplogb  26764  xrlimcnp  26946  gausslemma2dlem4  27348  cofcutr  27932  cofcutrtime  27935  addsproplem4  27980  addsproplem5  27981  addsproplem6  27982  addsuniflem  28009  negsproplem4  28039  negsproplem5  28040  negsproplem6  28041  mulsproplem12  28135  sltmuls1  28155  sltmuls2  28156  mulsuniflem  28157  precsexlem11  28225  twocut  28431  pw2cut2  28470  axlowdimlem8  29034  axlowdimlem11  29037  upgr1e  29198  uspgr1e  29329  wlkl1loop  29723  wlk1walk  29724  wlk2v2elem1  30242  frgrncvvdeqlem7  30392  hsn0elch  31335  rabsnel  32586  aciunf1lem  32751  gsumwrd2dccatlem  33170  cyc2fv1  33214  1arithidom  33629  ply1dg1rtn0  33673  vieta  33756  lvecdim0  33783  lvecendof1f1o  33810  repr0  34788  bnj97  35041  bnj553  35073  bnj966  35119  bnj1442  35224  fineqvinfep  35300  subfacp1lem2a  35393  subfacp1lem5  35397  cvmliftlem4  35501  fmla0xp  35596  prv1n  35644  bj-0eltag  37223  poimirlem3  37871  poimirlem9  37877  poimirlem31  37899  poimirlem32  37900  prdsbnd  38041  heiborlem3  38061  grposnOLD  38130  grpokerinj  38141  0idl  38273  0rngo  38275  sticksstones11  42523  0prjspnlem  42978  0prjspnrel  42982  fvilbdRP  44043  frege54cor1c  44268  binomcxplemnotnn0  44709  snsslVD  45181  snssl  45182  unipwrVD  45184  unipwr  45185  sucidALTVD  45222  sucidALT  45223  sucidVD  45224  unisnALT  45278  nregmodel  45370  eliuniincex  45465  cnrefiisplem  46184  0cnf  46232  qndenserrnbl  46650  nnfoctbdjlem  46810  isomenndlem  46885  hoidmvlelem2  46951  hoiqssbl  46980  tannpoly  47247  sinnpoly  47248  funressnfv  47400  el1fzopredsuc  47682  setsidel  47733  sbgoldbo  48144  lincval0  48772  lcoel0  48785  1arympt1  48995  discsubc  49420  setc1onsubc  49958  initocmd  50025