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 231	1 ⊢ 𝐴 ∈ {𝐴}

Syntax hints:   ∈ wcel 2119  Vcvv 3432  {csn 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-sn 4563

This theorem is referenced by:  vsnid  4602  rabsnt  4670  sseliALT  5238  0sn0ep  5529  opthprc  5689  dmsnsnsn  6178  snsn0non  6443  fvrn0  6862  fsn  7084  fsn2  7085  fnsnbOLD  7117  fmptsng  7119  fmptsnd  7120  fvsng  7131  ovima0  7542  brtpos0  8180  tfrlem11  8324  mapsncnv  8838  0elixp  8874  domunsncan  9012  enfixsn  9021  infeq5i  9555  tc2  9659  djulcl  9832  djurcl  9833  djulf1o  9834  djuun  9848  isfin4p1  10235  fin1a2lem12  10331  dcomex  10367  axdc3lem4  10373  zornn0g  10425  axpowndlem3  10520  canthp1lem2  10574  elreal2  11053  xrinfmss  13260  fseq1p1m1  13550  1exp  14051  wrdexb  14485  divalgmod  16373  0bits  16406  lcmfunsnlem2  16607  0ram  16989  setsid  17175  imasvscafn  17499  imasvscaval  17500  gsumval2  18652  0subm  18783  gsumz  18802  smndex1mnd  18879  smndex1id  18880  mulgfval  19043  psgnsn  19493  psgnprfval2  19496  c0snmhm  20441  pzriprnglem4  21466  pzriprnglem5  21467  pzriprnglem7  21469  pzriprnglem9  21471  pzriprnglem13  21475  pzriprnglem14  21476  pzriprng1ALT  21478  mat0dimscm  22459  mat0scmat  22528  mvmumamul1  22544  m1detdiag  22587  pmatcoe1fsupp  22691  d0mat2pmat  22728  pmatcollpw3fi1lem1  22776  pmatcollpw3fi1lem2  22777  chpmat0d  22824  dfac14  23608  filconn  23873  uffix  23911  cnextfvval  24055  cnextcn  24057  ust0  24210  bndth  24950  ehl1eudis  25412  minveclem4a  25422  dvef  25972  tdeglem2  26051  mdegcl  26059  aalioulem2  26324  cxplogb  26775  xrlimcnp  26957  gausslemma2dlem4  27357  cofcutr  27941  cofcutrtime  27944  addsproplem4  27989  addsproplem5  27990  addsproplem6  27991  addsuniflem  28018  negsproplem4  28048  negsproplem5  28049  negsproplem6  28050  mulsproplem12  28144  sltmuls1  28164  sltmuls2  28165  mulsuniflem  28166  precsexlem11  28234  twocut  28440  pw2cut2  28479  axlowdimlem8  29043  axlowdimlem11  29046  upgr1e  29207  uspgr1e  29338  wlkl1loop  29731  wlk1walk  29732  wlk2v2elem1  30250  frgrncvvdeqlem7  30400  hsn0elch  31344  rabsnel  32595  aciunf1lem  32761  gsumwrd2dccatlem  33165  cyc2fv1  33209  1arithidom  33627  ply1dg1rtn0  33671  0mplrim  33705  vieta  33771  lvecdim0  33798  lvecendof1f1o  33824  repr0  34802  bnj97  35055  bnj553  35087  bnj966  35133  bnj1442  35238  fineqvinfep  35313  subfacp1lem2a  35415  subfacp1lem5  35419  cvmliftlem4  35523  fmla0xp  35618  prv1n  35666  bj-0eltag  37338  poimirlem3  37997  poimirlem9  38003  poimirlem31  38025  poimirlem32  38026  prdsbnd  38167  heiborlem3  38187  grposnOLD  38256  grpokerinj  38267  0idl  38399  0rngo  38401  sticksstones11  42648  0prjspnlem  43080  0prjspnrel  43084  fvilbdRP  44141  frege54cor1c  44366  binomcxplemnotnn0  44807  snsslVD  45279  snssl  45280  unipwrVD  45282  unipwr  45283  sucidALTVD  45320  sucidALT  45321  sucidVD  45322  unisnALT  45376  nregmodel  45468  eliuniincex  45563  cnrefiisplem  46279  0cnf  46327  qndenserrnbl  46745  nnfoctbdjlem  46905  isomenndlem  46980  hoidmvlelem2  47046  hoiqssbl  47075  tannpoly  47360  sinnpoly  47361  funressnfv  47513  el1fzopredsuc  47796  setsidel  47858  sbgoldbo  48285  lincval0  48913  lcoel0  48926  1arympt1  49136  discsubc  49561  setc1onsubc  50099  initocmd  50166