Theorem snid 4663

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  {csn 4627

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-sn 4628

This theorem is referenced by:  vsnid  4664  rabsnt  4734  sseliALT  5308  intidOLD  5457  0sn0ep  5583  opthprc  5738  dmsnsnsn  6216  snsn0non  6486  fvrn0  6918  fsn  7128  fsn2  7129  fnsnb  7159  fmptsng  7161  fmptsnd  7162  fvsng  7173  ovima0  7581  brtpos0  8213  tfrlem11  8383  mapsncnv  8883  0elixp  8919  domunsncan  9068  enfixsn  9077  infeq5i  9627  tc2  9733  djulcl  9901  djurcl  9902  djulf1o  9903  djuun  9917  isfin4p1  10306  fin1a2lem12  10402  dcomex  10438  axdc3lem4  10444  zornn0g  10496  axpowndlem3  10590  canthp1lem2  10644  elreal2  11123  xrinfmss  13285  fseq1p1m1  13571  1exp  14053  wrdexb  14471  divalgmod  16345  0bits  16376  lcmfunsnlem2  16573  0ram  16949  setsid  17137  imasvscafn  17479  imasvscaval  17480  gsumval2  18601  0subm  18694  gsumz  18713  smndex1mnd  18787  smndex1id  18788  mulgfval  18946  psgnsn  19381  psgnprfval2  19384  mat0dimscm  21953  mat0scmat  22022  mvmumamul1  22038  m1detdiag  22081  pmatcoe1fsupp  22185  d0mat2pmat  22222  pmatcollpw3fi1lem1  22270  pmatcollpw3fi1lem2  22271  chpmat0d  22318  dfac14  23104  filconn  23369  uffix  23407  cnextfvval  23551  cnextcn  23553  ust0  23706  bndth  24456  ehl1eudis  24919  minveclem4a  24929  dvef  25479  tdeglem2  25561  mdegcl  25569  aalioulem2  25828  cxplogb  26271  xrlimcnp  26453  gausslemma2dlem4  26852  cofcutr  27391  cofcutrtime  27394  addsproplem4  27436  addsproplem5  27437  addsproplem6  27438  addsuniflem  27464  negsproplem4  27485  negsproplem5  27486  negsproplem6  27487  mulsproplem12  27563  ssltmul1  27582  ssltmul2  27583  mulsuniflem  27584  precsexlem11  27643  axlowdimlem8  28187  axlowdimlem11  28190  upgr1e  28353  uspgr1e  28481  wlkl1loop  28875  wlk1walk  28876  wlk2v2elem1  29388  frgrncvvdeqlem7  29538  hsn0elch  30479  rabsnel  31718  aciunf1lem  31865  cyc2fv1  32258  lvecdim0  32637  repr0  33561  bnj97  33815  bnj553  33847  bnj966  33893  bnj1442  33998  subfacp1lem2a  34109  subfacp1lem5  34113  cvmliftlem4  34217  fmla0xp  34312  prv1n  34360  bj-0eltag  35797  poimirlem3  36429  poimirlem9  36435  poimirlem31  36457  poimirlem32  36458  prdsbnd  36599  heiborlem3  36619  grposnOLD  36688  grpokerinj  36699  0idl  36831  0rngo  36833  sticksstones11  40910  0prjspnlem  41309  0prjspnrel  41313  fvilbdRP  42374  frege54cor1c  42599  binomcxplemnotnn0  43048  snsslVD  43523  snssl  43524  unipwrVD  43526  unipwr  43527  sucidALTVD  43564  sucidALT  43565  sucidVD  43566  unisnALT  43620  eliuniincex  43731  cnrefiisplem  44480  0cnf  44528  dvmptfprod  44596  qndenserrnbl  44946  nnfoctbdjlem  45106  isomenndlem  45181  hoidmvlelem2  45247  hoiqssbl  45276  funressnfv  45688  el1fzopredsuc  45968  setsidel  45979  sbgoldbo  46390  c0snmhm  46648  lincval0  46998  lcoel0  47011  1arympt1  47226