Theorem snid 4618

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-sn 4580

This theorem is referenced by:  vsnid  4619  rabsnt  4687  sseliALT  5256  0sn0ep  5547  opthprc  5707  dmsnsnsn  6201  snsn0non  6466  fvrn0  6889  fsn  7111  fsn2  7112  fnsnbOLD  7144  fmptsng  7146  fmptsnd  7147  fvsng  7158  ovima0  7569  brtpos0  8206  tfrlem11  8352  mapsncnv  8868  0elixp  8904  domunsncan  9042  enfixsn  9051  infeq5i  9584  tc2  9688  djulcl  9861  djurcl  9862  djulf1o  9863  djuun  9877  isfin4p1  10265  fin1a2lem12  10361  dcomex  10397  axdc3lem4  10403  zornn0g  10455  axpowndlem3  10550  canthp1lem2  10604  elreal2  11083  xrinfmss  13306  fseq1p1m1  13596  1exp  14097  wrdexb  14531  divalgmod  16430  0bits  16463  lcmfunsnlem2  16664  0ram  17046  setsid  17233  imasvscafn  17557  imasvscaval  17558  gsumval2  18710  0subm  18841  gsumz  18860  smndex1mnd  18937  smndex1id  18938  mulgfval  19101  psgnsn  19550  psgnprfval2  19553  c0snmhm  20498  pzriprnglem4  21523  pzriprnglem5  21524  pzriprnglem7  21526  pzriprnglem9  21528  pzriprnglem13  21532  pzriprnglem14  21533  pzriprng1ALT  21535  mat0dimscm  22516  mat0scmat  22585  mvmumamul1  22601  m1detdiag  22644  pmatcoe1fsupp  22748  d0mat2pmat  22785  pmatcollpw3fi1lem1  22833  pmatcollpw3fi1lem2  22834  chpmat0d  22881  dfac14  23665  filconn  23930  uffix  23968  cnextfvval  24112  cnextcn  24114  ust0  24267  bndth  25007  ehl1eudis  25469  minveclem4a  25479  dvef  26029  tdeglem2  26108  mdegcl  26116  aalioulem2  26384  cxplogb  26838  xrlimcnp  27020  gausslemma2dlem4  27420  cofcutr  28004  cofcutrtime  28007  addsproplem4  28052  addsproplem5  28053  addsproplem6  28054  addsuniflem  28081  negsproplem4  28111  negsproplem5  28112  negsproplem6  28113  mulsproplem12  28207  sltmuls1  28227  sltmuls2  28228  mulsuniflem  28229  precsexlem11  28297  twocut  28503  pw2cut2  28542  axlowdimlem8  29106  axlowdimlem11  29109  upgr1e  29270  uspgr1e  29401  wlkl1loop  29794  wlk1walk  29795  wlk2v2elem1  30313  frgrncvvdeqlem7  30463  hsn0elch  31407  rabsnel  32658  aciunf1lem  32824  gsumwrd2dccatlem  33217  cyc2fv1  33261  1arithidom  33693  ply1dg1rtn0  33737  0mplrim  33771  vieta  33837  lvecdim0  33864  lvecendof1f1o  33890  repr0  34865  bnj97  35121  bnj553  35153  bnj966  35199  bnj1442  35304  fineqvinfep  35381  subfacp1lem2a  35490  subfacp1lem5  35494  cvmliftlem4  35598  fmla0xp  35693  prv1n  35741  bj-0eltag  37423  poimirlem3  38082  poimirlem9  38088  poimirlem31  38110  poimirlem32  38111  prdsbnd  38252  heiborlem3  38272  grposnOLD  38341  grpokerinj  38352  0idl  38484  0rngo  38486  sticksstones11  42733  0prjspnlem  43165  0prjspnrel  43169  fvilbdRP  44226  frege54cor1c  44451  binomcxplemnotnn0  44892  snsslVD  45364  snssl  45365  unipwrVD  45367  unipwr  45368  sucidALTVD  45405  sucidALT  45406  sucidVD  45407  unisnALT  45461  nregmodel  45553  eliuniincex  45647  cnrefiisplem  46363  0cnf  46411  qndenserrnbl  46829  nnfoctbdjlem  46989  isomenndlem  47064  hoidmvlelem2  47130  hoiqssbl  47159  tannpoly  47444  sinnpoly  47445  funressnfv  47597  el1fzopredsuc  47880  setsidel  47942  sbgoldbo  48369  lincval0  48997  lcoel0  49010  1arympt1  49220  discsubc  49645  setc1onsubc  50183  initocmd  50250