Theorem snid 4623

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  {csn 4584

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-sn 4585

This theorem is used by:  vsnid  4624  rabsnt  4692  sseliALT  5263  0sn0ep  5555  opthprc  5715  dmsnsnsn  6214  snsn0non  6482  fvrn0  6905  fsn  7128  fsn2  7129  fnsnbOLD  7163  fmptsng  7165  fmptsnd  7166  fvsng  7177  ovima0  7592  brtpos0  8234  tfrlem11  8380  mapsncnv  8905  0elixp  8941  domunsncan  9080  enfixsn  9089  infeq5i  9621  tc2  9725  djulcl  9972  djurcl  9973  djulf1o  9974  djuun  9988  isfin4p1  10374  fin1a2lem12  10470  dcomex  10506  axdc3lem4  10512  zornn0g  10564  axpowndlem3  10665  canthp1lem2  10719  elreal2  11198  xrinfmss  13421  fseq1p1m1  13712  1exp  14214  wrdexb  14650  divalgmod  16556  0bits  16589  lcmfunsnlem2  16795  0ram  17178  setsid  17365  imasvscafn  17689  imasvscaval  17690  gsumval2  18855  0subm  18993  gsumz  19012  smndex1mnd  19089  smndex1id  19090  mulgfval  19259  psgnsn  19714  psgnprfval2  19717  c0snmhm  20673  pzriprnglem4  21770  pzriprnglem5  21771  pzriprnglem7  21773  pzriprnglem9  21775  pzriprnglem13  21779  pzriprnglem14  21780  pzriprng1ALT  21782  mat0dimscm  22764  mat0scmat  22833  mvmumamul1  22849  m1detdiag  22892  pmatcoe1fsupp  22999  d0mat2pmat  23036  pmatcollpw3fi1lem1  23084  pmatcollpw3fi1lem2  23085  chpmat0d  23132  dfac14  23917  filconn  24182  uffix  24220  cnextfvval  24364  cnextcn  24366  ust0  24519  bndth  25259  ehl1eudis  25721  minveclem4a  25731  dvef  26280  tdeglem2  26359  mdegcl  26367  aalioulem2  26642  cxplogb  27096  xrlimcnp  27278  gausslemma2dlem4  27678  cofcutr  28292  cofcutrtime  28295  addsproplem4  28340  addsproplem5  28341  addsproplem6  28342  addsuniflem  28369  negsproplem4  28399  negsproplem5  28400  negsproplem6  28401  mulsproplem12  28495  sltmuls1  28515  sltmuls2  28516  mulsuniflem  28517  precsexlem11  28585  twocut  28791  pw2cut2  28830  axlowdimlem8  29509  axlowdimlem11  29512  upgr1e  29673  uspgr1e  29807  wlkl1loop  30200  wlk1walk  30201  wlk2v2elem1  30738  frgrncvvdeqlem7  30888  hsn0elch  31832  rabsnel  33078  aciunf1lem  33238  gsumwrd2dccatlem  33620  cyc2fv1  33664  1arithidom  34051  ply1dg1rtn0  34095  0mplrim  34128  vieta  34194  lvecdim0  34221  lvecendof1f1o  34247  repr0  35223  bnj97  35479  bnj553  35511  bnj966  35557  bnj1442  35662  fineqvinfep  35766  subfacp1lem2a  35914  subfacp1lem5  35918  cvmliftlem4  36022  fmla0xp  36117  prv1n  36165  bj-0eltag  37861  poimirlem3  38509  poimirlem9  38515  poimirlem31  38537  poimirlem32  38538  prdsbnd  38695  heiborlem3  38715  grposnOLD  38784  grpokerinj  38795  0idl  38927  0rngo  38929  sticksstones11  43174  0prjspnlem  43613  0prjspnrel  43617  fvilbdRP  44649  frege54cor1c  44874  binomcxplemnotnn0  45299  snsslVD  45770  snssl  45771  unipwrVD  45773  unipwr  45774  sucidALTVD  45811  sucidALT  45812  sucidVD  45813  unisnALT  45867  nregmodel  45959  eliuniincex  46067  cnrefiisplem  46783  0cnf  46831  qndenserrnbl  47249  nnfoctbdjlem  47409  isomenndlem  47484  hoidmvlelem2  47550  hoiqssbl  47579  tannpoly  47884  sinnpoly  47885  funressnfv  48057  el1fzopredsuc  48340  setsidel  48402  sbgoldbo  48829  lincval0  49471  lcoel0  49484  1arympt1  49694  discsubc  50116  setc1onsubc  50654  initocmd  50721