Theorem snid 4597

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

Syntax hints:   ∈ wcel 2106  Vcvv 3432  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-sn 4562

This theorem is referenced by:  vsnid  4598  rabsnt  4667  sseliALT  5233  elALT  5358  intid  5373  0sn0ep  5499  opthprc  5651  dmsnsnsn  6123  snsn0non  6385  fvrn0  6802  fsn  7007  fsn2  7008  fnsnb  7038  fmptsng  7040  fmptsnd  7041  fvsng  7052  ovima0  7451  brtpos0  8049  tfrlem11  8219  mapsncnv  8681  0elixp  8717  domunsncan  8859  enfixsn  8868  infeq5i  9394  tc2  9500  djulcl  9668  djurcl  9669  djulf1o  9670  djuun  9684  isfin4p1  10071  fin1a2lem12  10167  dcomex  10203  axdc3lem4  10209  zornn0g  10261  axpowndlem3  10355  canthp1lem2  10409  elreal2  10888  xrinfmss  13044  fseq1p1m1  13330  1exp  13812  wrdexb  14228  divalgmod  16115  0bits  16146  lcmfunsnlem2  16345  0ram  16721  setsid  16909  imasvscafn  17248  imasvscaval  17249  gsumval2  18370  0subm  18456  gsumz  18474  smndex1mnd  18549  smndex1id  18550  mulgfval  18702  psgnsn  19128  psgnprfval2  19131  mat0dimscm  21618  mat0scmat  21687  mvmumamul1  21703  m1detdiag  21746  pmatcoe1fsupp  21850  d0mat2pmat  21887  pmatcollpw3fi1lem1  21935  pmatcollpw3fi1lem2  21936  chpmat0d  21983  dfac14  22769  filconn  23034  uffix  23072  cnextfvval  23216  cnextcn  23218  ust0  23371  bndth  24121  ehl1eudis  24584  minveclem4a  24594  dvef  25144  tdeglem2  25226  mdegcl  25234  aalioulem2  25493  cxplogb  25936  xrlimcnp  26118  gausslemma2dlem4  26517  axlowdimlem8  27317  axlowdimlem11  27320  upgr1e  27483  uspgr1e  27611  wlkl1loop  28005  wlk1walk  28006  wlk2v2elem1  28519  frgrncvvdeqlem7  28669  hsn0elch  29610  rabsnel  30847  aciunf1lem  30999  cyc2fv1  31388  lvecdim0  31690  repr0  32591  bnj97  32846  bnj553  32878  bnj966  32924  bnj1442  33029  subfacp1lem2a  33142  subfacp1lem5  33146  cvmliftlem4  33250  fmla0xp  33345  prv1n  33393  cofcutr  34092  cofcutrtime  34093  bj-0eltag  35168  poimirlem3  35780  poimirlem9  35786  poimirlem31  35808  poimirlem32  35809  prdsbnd  35951  heiborlem3  35971  grposnOLD  36040  grpokerinj  36051  0idl  36183  0rngo  36185  sticksstones11  40112  0prjspnlem  40460  0prjspnrel  40464  fvilbdRP  41298  frege54cor1c  41523  binomcxplemnotnn0  41974  snsslVD  42449  snssl  42450  unipwrVD  42452  unipwr  42453  sucidALTVD  42490  sucidALT  42491  sucidVD  42492  unisnALT  42546  eliuniincex  42659  cnrefiisplem  43370  0cnf  43418  dvmptfprod  43486  qndenserrnbl  43836  nnfoctbdjlem  43993  isomenndlem  44068  hoidmvlelem2  44134  hoiqssbl  44163  funressnfv  44537  el1fzopredsuc  44817  setsidel  44828  sbgoldbo  45239  c0snmhm  45473  lincval0  45756  lcoel0  45769  1arympt1  45984