Theorem snid 4607

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-sn 4569

This theorem is referenced by:  vsnid  4608  rabsnt  4676  sseliALT  5244  0sn0ep  5528  opthprc  5688  dmsnsnsn  6178  snsn0non  6443  fvrn0  6862  fsn  7082  fsn2  7083  fnsnbOLD  7114  fmptsng  7116  fmptsnd  7117  fvsng  7128  ovima0  7539  brtpos0  8176  tfrlem11  8320  mapsncnv  8834  0elixp  8870  domunsncan  9008  enfixsn  9017  infeq5i  9548  tc2  9652  djulcl  9825  djurcl  9826  djulf1o  9827  djuun  9841  isfin4p1  10228  fin1a2lem12  10324  dcomex  10360  axdc3lem4  10366  zornn0g  10418  axpowndlem3  10513  canthp1lem2  10567  elreal2  11046  xrinfmss  13253  fseq1p1m1  13543  1exp  14044  wrdexb  14478  divalgmod  16366  0bits  16399  lcmfunsnlem2  16600  0ram  16982  setsid  17168  imasvscafn  17492  imasvscaval  17493  gsumval2  18645  0subm  18776  gsumz  18795  smndex1mnd  18872  smndex1id  18873  mulgfval  19036  psgnsn  19486  psgnprfval2  19489  c0snmhm  20434  pzriprnglem4  21474  pzriprnglem5  21475  pzriprnglem7  21477  pzriprnglem9  21479  pzriprnglem13  21483  pzriprnglem14  21484  pzriprng1ALT  21486  mat0dimscm  22444  mat0scmat  22513  mvmumamul1  22529  m1detdiag  22572  pmatcoe1fsupp  22676  d0mat2pmat  22713  pmatcollpw3fi1lem1  22761  pmatcollpw3fi1lem2  22762  chpmat0d  22809  dfac14  23593  filconn  23858  uffix  23896  cnextfvval  24040  cnextcn  24042  ust0  24195  bndth  24935  ehl1eudis  25397  minveclem4a  25407  dvef  25957  tdeglem2  26036  mdegcl  26044  aalioulem2  26310  cxplogb  26763  xrlimcnp  26945  gausslemma2dlem4  27346  cofcutr  27930  cofcutrtime  27933  addsproplem4  27978  addsproplem5  27979  addsproplem6  27980  addsuniflem  28007  negsproplem4  28037  negsproplem5  28038  negsproplem6  28039  mulsproplem12  28133  sltmuls1  28153  sltmuls2  28154  mulsuniflem  28155  precsexlem11  28223  twocut  28429  pw2cut2  28468  axlowdimlem8  29032  axlowdimlem11  29035  upgr1e  29196  uspgr1e  29327  wlkl1loop  29721  wlk1walk  29722  wlk2v2elem1  30240  frgrncvvdeqlem7  30390  hsn0elch  31334  rabsnel  32585  aciunf1lem  32750  gsumwrd2dccatlem  33153  cyc2fv1  33197  1arithidom  33612  ply1dg1rtn0  33656  vieta  33739  lvecdim0  33766  lvecendof1f1o  33793  repr0  34771  bnj97  35024  bnj553  35056  bnj966  35102  bnj1442  35207  fineqvinfep  35285  subfacp1lem2a  35378  subfacp1lem5  35382  cvmliftlem4  35486  fmla0xp  35581  prv1n  35629  bj-0eltag  37301  poimirlem3  37958  poimirlem9  37964  poimirlem31  37986  poimirlem32  37987  prdsbnd  38128  heiborlem3  38148  grposnOLD  38217  grpokerinj  38228  0idl  38360  0rngo  38362  sticksstones11  42609  0prjspnlem  43070  0prjspnrel  43074  fvilbdRP  44135  frege54cor1c  44360  binomcxplemnotnn0  44801  snsslVD  45273  snssl  45274  unipwrVD  45276  unipwr  45277  sucidALTVD  45314  sucidALT  45315  sucidVD  45316  unisnALT  45370  nregmodel  45462  eliuniincex  45557  cnrefiisplem  46275  0cnf  46323  qndenserrnbl  46741  nnfoctbdjlem  46901  isomenndlem  46976  hoidmvlelem2  47042  hoiqssbl  47071  tannpoly  47350  sinnpoly  47351  funressnfv  47503  el1fzopredsuc  47786  setsidel  47848  sbgoldbo  48275  lincval0  48903  lcoel0  48916  1arympt1  49126  discsubc  49551  setc1onsubc  50089  initocmd  50156