Theorem snid 4633

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458  {csn 4594

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-sn 4595

This theorem is used by:  vsnid  4634  rabsnt  4702  sseliALT  5277  0sn0ep  5570  opthprc  5730  dmsnsnsn  6226  snsn0non  6494  fvrn0  6916  fsn  7138  fsn2  7139  fnsnbOLD  7171  fmptsng  7173  fmptsnd  7174  fvsng  7185  ovima0  7602  brtpos0  8238  tfrlem11  8384  mapsncnv  8900  0elixp  8936  domunsncan  9075  enfixsn  9084  infeq5i  9615  tc2  9719  djulcl  9915  djurcl  9916  djulf1o  9917  djuun  9931  isfin4p1  10317  fin1a2lem12  10413  dcomex  10449  axdc3lem4  10455  zornn0g  10507  axpowndlem3  10602  canthp1lem2  10656  elreal2  11135  xrinfmss  13354  fseq1p1m1  13645  1exp  14147  wrdexb  14582  divalgmod  16489  0bits  16522  lcmfunsnlem2  16723  0ram  17105  setsid  17292  imasvscafn  17616  imasvscaval  17617  gsumval2  18773  0subm  18907  gsumz  18926  smndex1mnd  19003  smndex1id  19004  mulgfval  19166  psgnsn  19621  psgnprfval2  19624  c0snmhm  20578  pzriprnglem4  21671  pzriprnglem5  21672  pzriprnglem7  21674  pzriprnglem9  21676  pzriprnglem13  21680  pzriprnglem14  21681  pzriprng1ALT  21683  mat0dimscm  22663  mat0scmat  22732  mvmumamul1  22748  m1detdiag  22791  pmatcoe1fsupp  22895  d0mat2pmat  22932  pmatcollpw3fi1lem1  22980  pmatcollpw3fi1lem2  22981  chpmat0d  23028  dfac14  23812  filconn  24077  uffix  24115  cnextfvval  24259  cnextcn  24261  ust0  24414  bndth  25154  ehl1eudis  25616  minveclem4a  25626  dvef  26176  tdeglem2  26255  mdegcl  26263  aalioulem2  26533  cxplogb  26988  xrlimcnp  27170  gausslemma2dlem4  27570  cofcutr  28154  cofcutrtime  28157  addsproplem4  28202  addsproplem5  28203  addsproplem6  28204  addsuniflem  28231  negsproplem4  28261  negsproplem5  28262  negsproplem6  28263  mulsproplem12  28357  sltmuls1  28377  sltmuls2  28378  mulsuniflem  28379  precsexlem11  28447  twocut  28653  pw2cut2  28692  axlowdimlem8  29336  axlowdimlem11  29339  upgr1e  29500  uspgr1e  29631  wlkl1loop  30024  wlk1walk  30025  wlk2v2elem1  30543  frgrncvvdeqlem7  30693  hsn0elch  31637  rabsnel  32883  aciunf1lem  33044  gsumwrd2dccatlem  33428  cyc2fv1  33472  1arithidom  33858  ply1dg1rtn0  33902  0mplrim  33935  vieta  34001  lvecdim0  34028  lvecendof1f1o  34054  repr0  35030  bnj97  35286  bnj553  35318  bnj966  35364  bnj1442  35469  fineqvinfep  35562  subfacp1lem2a  35693  subfacp1lem5  35697  cvmliftlem4  35801  fmla0xp  35896  prv1n  35944  bj-0eltag  37655  poimirlem3  38315  poimirlem9  38321  poimirlem31  38343  poimirlem32  38344  prdsbnd  38485  heiborlem3  38505  grposnOLD  38574  grpokerinj  38585  0idl  38717  0rngo  38719  sticksstones11  42964  0prjspnlem  43396  0prjspnrel  43400  fvilbdRP  44457  frege54cor1c  44682  binomcxplemnotnn0  45107  snsslVD  45578  snssl  45579  unipwrVD  45581  unipwr  45582  sucidALTVD  45619  sucidALT  45620  sucidVD  45621  unisnALT  45675  nregmodel  45767  eliuniincex  45868  cnrefiisplem  46584  0cnf  46632  qndenserrnbl  47050  nnfoctbdjlem  47210  isomenndlem  47285  hoidmvlelem2  47351  hoiqssbl  47380  tannpoly  47668  sinnpoly  47669  funressnfv  47821  el1fzopredsuc  48104  setsidel  48166  sbgoldbo  48593  lincval0  49236  lcoel0  49249  1arympt1  49459  discsubc  49883  setc1onsubc  50421  initocmd  50488