Theorem snid 4643

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

Syntax hints:   ∈ wcel 2109  Vcvv 3464  {csn 4606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-sn 4607

This theorem is referenced by:  vsnid  4644  rabsnt  4712  sseliALT  5284  intidOLD  5438  0sn0ep  5562  opthprc  5723  dmsnsnsn  6214  snsn0non  6484  fvrn0  6911  fsn  7130  fsn2  7131  fnsnbOLD  7163  fmptsng  7165  fmptsnd  7166  fvsng  7177  ovima0  7591  brtpos0  8237  tfrlem11  8407  mapsncnv  8912  0elixp  8948  domunsncan  9091  enfixsn  9100  infeq5i  9655  tc2  9761  djulcl  9929  djurcl  9930  djulf1o  9931  djuun  9945  isfin4p1  10334  fin1a2lem12  10430  dcomex  10466  axdc3lem4  10472  zornn0g  10524  axpowndlem3  10618  canthp1lem2  10672  elreal2  11151  xrinfmss  13331  fseq1p1m1  13620  1exp  14114  wrdexb  14548  divalgmod  16430  0bits  16463  lcmfunsnlem2  16664  0ram  17045  setsid  17231  imasvscafn  17556  imasvscaval  17557  gsumval2  18669  0subm  18800  gsumz  18819  smndex1mnd  18893  smndex1id  18894  mulgfval  19057  psgnsn  19506  psgnprfval2  19509  c0snmhm  20428  pzriprnglem4  21450  pzriprnglem5  21451  pzriprnglem7  21453  pzriprnglem9  21455  pzriprnglem13  21459  pzriprnglem14  21460  pzriprng1ALT  21462  mat0dimscm  22412  mat0scmat  22481  mvmumamul1  22497  m1detdiag  22540  pmatcoe1fsupp  22644  d0mat2pmat  22681  pmatcollpw3fi1lem1  22729  pmatcollpw3fi1lem2  22730  chpmat0d  22777  dfac14  23561  filconn  23826  uffix  23864  cnextfvval  24008  cnextcn  24010  ust0  24163  bndth  24913  ehl1eudis  25377  minveclem4a  25387  dvef  25941  tdeglem2  26023  mdegcl  26031  aalioulem2  26298  cxplogb  26753  xrlimcnp  26935  gausslemma2dlem4  27337  cofcutr  27889  cofcutrtime  27892  addsproplem4  27936  addsproplem5  27937  addsproplem6  27938  addsuniflem  27965  negsproplem4  27994  negsproplem5  27995  negsproplem6  27996  mulsproplem12  28087  ssltmul1  28107  ssltmul2  28108  mulsuniflem  28109  precsexlem11  28176  twocut  28366  axlowdimlem8  28933  axlowdimlem11  28936  upgr1e  29097  uspgr1e  29228  wlkl1loop  29623  wlk1walk  29624  wlk2v2elem1  30141  frgrncvvdeqlem7  30291  hsn0elch  31234  rabsnel  32486  aciunf1lem  32645  gsumwrd2dccatlem  33065  cyc2fv1  33137  1arithidom  33557  ply1dg1rtn0  33598  lvecdim0  33651  lvecendof1f1o  33678  repr0  34648  bnj97  34902  bnj553  34934  bnj966  34980  bnj1442  35085  subfacp1lem2a  35207  subfacp1lem5  35211  cvmliftlem4  35315  fmla0xp  35410  prv1n  35458  bj-0eltag  37001  poimirlem3  37652  poimirlem9  37658  poimirlem31  37680  poimirlem32  37681  prdsbnd  37822  heiborlem3  37842  grposnOLD  37911  grpokerinj  37922  0idl  38054  0rngo  38056  sticksstones11  42174  0prjspnlem  42621  0prjspnrel  42625  fvilbdRP  43689  frege54cor1c  43914  binomcxplemnotnn0  44355  snsslVD  44828  snssl  44829  unipwrVD  44831  unipwr  44832  sucidALTVD  44869  sucidALT  44870  sucidVD  44871  unisnALT  44925  nregmodel  45017  eliuniincex  45113  cnrefiisplem  45838  0cnf  45886  qndenserrnbl  46304  nnfoctbdjlem  46464  isomenndlem  46539  hoidmvlelem2  46605  hoiqssbl  46634  funressnfv  47052  el1fzopredsuc  47334  setsidel  47370  sbgoldbo  47781  lincval0  48371  lcoel0  48384  1arympt1  48598  discsubc  49011  setc1onsubc  49459