Theorem snid 4667

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

Syntax hints:   ∈ wcel 2106  Vcvv 3478  {csn 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-sn 4632

This theorem is referenced by:  vsnid  4668  rabsnt  4736  sseliALT  5315  intidOLD  5469  0sn0ep  5593  opthprc  5753  dmsnsnsn  6242  snsn0non  6511  fvrn0  6937  fsn  7155  fsn2  7156  fnsnb  7186  fmptsng  7188  fmptsnd  7189  fvsng  7200  ovima0  7612  brtpos0  8257  tfrlem11  8427  mapsncnv  8932  0elixp  8968  domunsncan  9111  enfixsn  9120  infeq5i  9674  tc2  9780  djulcl  9948  djurcl  9949  djulf1o  9950  djuun  9964  isfin4p1  10353  fin1a2lem12  10449  dcomex  10485  axdc3lem4  10491  zornn0g  10543  axpowndlem3  10637  canthp1lem2  10691  elreal2  11170  xrinfmss  13349  fseq1p1m1  13635  1exp  14129  wrdexb  14560  divalgmod  16440  0bits  16473  lcmfunsnlem2  16674  0ram  17054  setsid  17242  imasvscafn  17584  imasvscaval  17585  gsumval2  18712  0subm  18843  gsumz  18862  smndex1mnd  18936  smndex1id  18937  mulgfval  19100  psgnsn  19553  psgnprfval2  19556  c0snmhm  20480  pzriprnglem4  21513  pzriprnglem5  21514  pzriprnglem7  21516  pzriprnglem9  21518  pzriprnglem13  21522  pzriprnglem14  21523  pzriprng1ALT  21525  mat0dimscm  22491  mat0scmat  22560  mvmumamul1  22576  m1detdiag  22619  pmatcoe1fsupp  22723  d0mat2pmat  22760  pmatcollpw3fi1lem1  22808  pmatcollpw3fi1lem2  22809  chpmat0d  22856  dfac14  23642  filconn  23907  uffix  23945  cnextfvval  24089  cnextcn  24091  ust0  24244  bndth  25004  ehl1eudis  25468  minveclem4a  25478  dvef  26033  tdeglem2  26115  mdegcl  26123  aalioulem2  26390  cxplogb  26844  xrlimcnp  27026  gausslemma2dlem4  27428  cofcutr  27973  cofcutrtime  27976  addsproplem4  28020  addsproplem5  28021  addsproplem6  28022  addsuniflem  28049  negsproplem4  28078  negsproplem5  28079  negsproplem6  28080  mulsproplem12  28168  ssltmul1  28188  ssltmul2  28189  mulsuniflem  28190  precsexlem11  28256  axlowdimlem8  28979  axlowdimlem11  28982  upgr1e  29145  uspgr1e  29276  wlkl1loop  29671  wlk1walk  29672  wlk2v2elem1  30184  frgrncvvdeqlem7  30334  hsn0elch  31277  rabsnel  32528  aciunf1lem  32679  gsumwrd2dccatlem  33052  cyc2fv1  33124  1arithidom  33545  ply1dg1rtn0  33585  lvecdim0  33634  lvecendof1f1o  33661  repr0  34605  bnj97  34859  bnj553  34891  bnj966  34937  bnj1442  35042  subfacp1lem2a  35165  subfacp1lem5  35169  cvmliftlem4  35273  fmla0xp  35368  prv1n  35416  bj-0eltag  36961  poimirlem3  37610  poimirlem9  37616  poimirlem31  37638  poimirlem32  37639  prdsbnd  37780  heiborlem3  37800  grposnOLD  37869  grpokerinj  37880  0idl  38012  0rngo  38014  sticksstones11  42138  0prjspnlem  42610  0prjspnrel  42614  fvilbdRP  43680  frege54cor1c  43905  binomcxplemnotnn0  44352  snsslVD  44827  snssl  44828  unipwrVD  44830  unipwr  44831  sucidALTVD  44868  sucidALT  44869  sucidVD  44870  unisnALT  44924  eliuniincex  45049  cnrefiisplem  45785  0cnf  45833  qndenserrnbl  46251  nnfoctbdjlem  46411  isomenndlem  46486  hoidmvlelem2  46552  hoiqssbl  46581  funressnfv  46993  el1fzopredsuc  47275  setsidel  47301  sbgoldbo  47712  lincval0  48261  lcoel0  48274  1arympt1  48488