Theorem snid 4644

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

Syntax hints:   ∈ wcel 2107  Vcvv 3464  {csn 4608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3466  df-sn 4609

This theorem is referenced by:  vsnid  4645  rabsnt  4713  sseliALT  5291  intidOLD  5445  0sn0ep  5570  opthprc  5731  dmsnsnsn  6222  snsn0non  6490  fvrn0  6917  fsn  7136  fsn2  7137  fnsnbOLD  7169  fmptsng  7171  fmptsnd  7172  fvsng  7183  ovima0  7595  brtpos0  8241  tfrlem11  8411  mapsncnv  8916  0elixp  8952  domunsncan  9095  enfixsn  9104  infeq5i  9659  tc2  9765  djulcl  9933  djurcl  9934  djulf1o  9935  djuun  9949  isfin4p1  10338  fin1a2lem12  10434  dcomex  10470  axdc3lem4  10476  zornn0g  10528  axpowndlem3  10622  canthp1lem2  10676  elreal2  11155  xrinfmss  13335  fseq1p1m1  13621  1exp  14115  wrdexb  14546  divalgmod  16426  0bits  16459  lcmfunsnlem2  16660  0ram  17041  setsid  17227  imasvscafn  17558  imasvscaval  17559  gsumval2  18673  0subm  18804  gsumz  18823  smndex1mnd  18897  smndex1id  18898  mulgfval  19061  psgnsn  19511  psgnprfval2  19514  c0snmhm  20436  pzriprnglem4  21462  pzriprnglem5  21463  pzriprnglem7  21465  pzriprnglem9  21467  pzriprnglem13  21471  pzriprnglem14  21472  pzriprng1ALT  21474  mat0dimscm  22442  mat0scmat  22511  mvmumamul1  22527  m1detdiag  22570  pmatcoe1fsupp  22674  d0mat2pmat  22711  pmatcollpw3fi1lem1  22759  pmatcollpw3fi1lem2  22760  chpmat0d  22807  dfac14  23591  filconn  23856  uffix  23894  cnextfvval  24038  cnextcn  24040  ust0  24193  bndth  24945  ehl1eudis  25409  minveclem4a  25419  dvef  25973  tdeglem2  26055  mdegcl  26063  aalioulem2  26330  cxplogb  26784  xrlimcnp  26966  gausslemma2dlem4  27368  cofcutr  27913  cofcutrtime  27916  addsproplem4  27960  addsproplem5  27961  addsproplem6  27962  addsuniflem  27989  negsproplem4  28018  negsproplem5  28019  negsproplem6  28020  mulsproplem12  28108  ssltmul1  28128  ssltmul2  28129  mulsuniflem  28130  precsexlem11  28196  axlowdimlem8  28913  axlowdimlem11  28916  upgr1e  29077  uspgr1e  29208  wlkl1loop  29603  wlk1walk  29604  wlk2v2elem1  30121  frgrncvvdeqlem7  30271  hsn0elch  31214  rabsnel  32466  aciunf1lem  32619  gsumwrd2dccatlem  33015  cyc2fv1  33087  1arithidom  33506  ply1dg1rtn0  33546  lvecdim0  33598  lvecendof1f1o  33625  repr0  34567  bnj97  34821  bnj553  34853  bnj966  34899  bnj1442  35004  subfacp1lem2a  35126  subfacp1lem5  35130  cvmliftlem4  35234  fmla0xp  35329  prv1n  35377  bj-0eltag  36920  poimirlem3  37571  poimirlem9  37577  poimirlem31  37599  poimirlem32  37600  prdsbnd  37741  heiborlem3  37761  grposnOLD  37830  grpokerinj  37841  0idl  37973  0rngo  37975  sticksstones11  42098  0prjspnlem  42578  0prjspnrel  42582  fvilbdRP  43648  frege54cor1c  43873  binomcxplemnotnn0  44320  snsslVD  44794  snssl  44795  unipwrVD  44797  unipwr  44798  sucidALTVD  44835  sucidALT  44836  sucidVD  44837  unisnALT  44891  eliuniincex  45059  cnrefiisplem  45789  0cnf  45837  qndenserrnbl  46255  nnfoctbdjlem  46415  isomenndlem  46490  hoidmvlelem2  46556  hoiqssbl  46585  funressnfv  47001  el1fzopredsuc  47283  setsidel  47309  sbgoldbo  47720  lincval0  48278  lcoel0  48291  1arympt1  48505