Theorem snid 4629

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  {csn 4590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-sn 4591

This theorem is referenced by:  vsnid  4630  rabsnt  4698  sseliALT  5273  0sn0ep  5567  opthprc  5727  dmsnsnsn  6223  snsn0non  6489  fvrn0  6911  fsn  7133  fsn2  7134  fnsnbOLD  7166  fmptsng  7168  fmptsnd  7169  fvsng  7180  ovima0  7591  brtpos0  8230  tfrlem11  8376  mapsncnv  8892  0elixp  8928  domunsncan  9066  enfixsn  9075  infeq5i  9606  tc2  9710  djulcl  9897  djurcl  9898  djulf1o  9899  djuun  9913  isfin4p1  10300  fin1a2lem12  10396  dcomex  10432  axdc3lem4  10438  zornn0g  10490  axpowndlem3  10585  canthp1lem2  10639  elreal2  11118  xrinfmss  13337  fseq1p1m1  13628  1exp  14129  wrdexb  14564  divalgmod  16465  0bits  16498  lcmfunsnlem2  16699  0ram  17081  setsid  17268  imasvscafn  17592  imasvscaval  17593  gsumval2  18745  0subm  18877  gsumz  18896  smndex1mnd  18973  smndex1id  18974  mulgfval  19136  psgnsn  19591  psgnprfval2  19594  c0snmhm  20546  pzriprnglem4  21615  pzriprnglem5  21616  pzriprnglem7  21618  pzriprnglem9  21620  pzriprnglem13  21624  pzriprnglem14  21625  pzriprng1ALT  21627  mat0dimscm  22607  mat0scmat  22676  mvmumamul1  22692  m1detdiag  22735  pmatcoe1fsupp  22839  d0mat2pmat  22876  pmatcollpw3fi1lem1  22924  pmatcollpw3fi1lem2  22925  chpmat0d  22972  dfac14  23756  filconn  24021  uffix  24059  cnextfvval  24203  cnextcn  24205  ust0  24358  bndth  25098  ehl1eudis  25560  minveclem4a  25570  dvef  26120  tdeglem2  26199  mdegcl  26207  aalioulem2  26477  cxplogb  26932  xrlimcnp  27114  gausslemma2dlem4  27514  cofcutr  28098  cofcutrtime  28101  addsproplem4  28146  addsproplem5  28147  addsproplem6  28148  addsuniflem  28175  negsproplem4  28205  negsproplem5  28206  negsproplem6  28207  mulsproplem12  28301  sltmuls1  28321  sltmuls2  28322  mulsuniflem  28323  precsexlem11  28391  twocut  28597  pw2cut2  28636  axlowdimlem8  29280  axlowdimlem11  29283  upgr1e  29444  uspgr1e  29575  wlkl1loop  29968  wlk1walk  29969  wlk2v2elem1  30487  frgrncvvdeqlem7  30637  hsn0elch  31581  rabsnel  32827  aciunf1lem  32988  gsumwrd2dccatlem  33378  cyc2fv1  33422  1arithidom  33808  ply1dg1rtn0  33852  0mplrim  33885  vieta  33951  lvecdim0  33978  lvecendof1f1o  34004  repr0  34979  bnj97  35235  bnj553  35267  bnj966  35313  bnj1442  35418  fineqvinfep  35519  subfacp1lem2a  35653  subfacp1lem5  35657  cvmliftlem4  35761  fmla0xp  35856  prv1n  35904  bj-0eltag  37595  poimirlem3  38255  poimirlem9  38261  poimirlem31  38283  poimirlem32  38284  prdsbnd  38425  heiborlem3  38445  grposnOLD  38514  grpokerinj  38525  0idl  38657  0rngo  38659  sticksstones11  42904  0prjspnlem  43338  0prjspnrel  43342  fvilbdRP  44399  frege54cor1c  44624  binomcxplemnotnn0  45049  snsslVD  45520  snssl  45521  unipwrVD  45523  unipwr  45524  sucidALTVD  45561  sucidALT  45562  sucidVD  45563  unisnALT  45617  nregmodel  45709  eliuniincex  45810  cnrefiisplem  46526  0cnf  46574  qndenserrnbl  46992  nnfoctbdjlem  47152  isomenndlem  47227  hoidmvlelem2  47293  hoiqssbl  47322  tannpoly  47610  sinnpoly  47611  funressnfv  47763  el1fzopredsuc  48046  setsidel  48108  sbgoldbo  48535  lincval0  49178  lcoel0  49191  1arympt1  49401  discsubc  49825  setc1onsubc  50363  initocmd  50430