Theorem snid 4616

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

Syntax hints:   ∈ wcel 2113  Vcvv 3437  {csn 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-sn 4578

This theorem is referenced by:  vsnid  4617  rabsnt  4685  sseliALT  5251  0sn0ep  5525  opthprc  5685  dmsnsnsn  6174  snsn0non  6439  fvrn0  6858  fsn  7076  fsn2  7077  fnsnbOLD  7108  fmptsng  7110  fmptsnd  7111  fvsng  7122  ovima0  7533  brtpos0  8171  tfrlem11  8315  mapsncnv  8825  0elixp  8861  domunsncan  8999  enfixsn  9008  infeq5i  9535  tc2  9639  djulcl  9812  djurcl  9813  djulf1o  9814  djuun  9828  isfin4p1  10215  fin1a2lem12  10311  dcomex  10347  axdc3lem4  10353  zornn0g  10405  axpowndlem3  10499  canthp1lem2  10553  elreal2  11032  xrinfmss  13213  fseq1p1m1  13502  1exp  14002  wrdexb  14436  divalgmod  16321  0bits  16354  lcmfunsnlem2  16555  0ram  16936  setsid  17122  imasvscafn  17445  imasvscaval  17446  gsumval2  18598  0subm  18729  gsumz  18748  smndex1mnd  18822  smndex1id  18823  mulgfval  18986  psgnsn  19436  psgnprfval2  19439  c0snmhm  20385  pzriprnglem4  21425  pzriprnglem5  21426  pzriprnglem7  21428  pzriprnglem9  21430  pzriprnglem13  21434  pzriprnglem14  21435  pzriprng1ALT  21437  mat0dimscm  22387  mat0scmat  22456  mvmumamul1  22472  m1detdiag  22515  pmatcoe1fsupp  22619  d0mat2pmat  22656  pmatcollpw3fi1lem1  22704  pmatcollpw3fi1lem2  22705  chpmat0d  22752  dfac14  23536  filconn  23801  uffix  23839  cnextfvval  23983  cnextcn  23985  ust0  24138  bndth  24887  ehl1eudis  25350  minveclem4a  25360  dvef  25914  tdeglem2  25996  mdegcl  26004  aalioulem2  26271  cxplogb  26726  xrlimcnp  26908  gausslemma2dlem4  27310  cofcutr  27871  cofcutrtime  27874  addsproplem4  27918  addsproplem5  27919  addsproplem6  27920  addsuniflem  27947  negsproplem4  27976  negsproplem5  27977  negsproplem6  27978  mulsproplem12  28069  ssltmul1  28089  ssltmul2  28090  mulsuniflem  28091  precsexlem11  28158  twocut  28349  pw2cut2  28385  axlowdimlem8  28931  axlowdimlem11  28934  upgr1e  29095  uspgr1e  29226  wlkl1loop  29620  wlk1walk  29621  wlk2v2elem1  30139  frgrncvvdeqlem7  30289  hsn0elch  31232  rabsnel  32484  aciunf1lem  32648  gsumwrd2dccatlem  33055  cyc2fv1  33099  1arithidom  33511  ply1dg1rtn0  33553  lvecdim0  33642  lvecendof1f1o  33669  repr0  34647  bnj97  34901  bnj553  34933  bnj966  34979  bnj1442  35084  subfacp1lem2a  35247  subfacp1lem5  35251  cvmliftlem4  35355  fmla0xp  35450  prv1n  35498  bj-0eltag  37045  poimirlem3  37686  poimirlem9  37692  poimirlem31  37714  poimirlem32  37715  prdsbnd  37856  heiborlem3  37876  grposnOLD  37945  grpokerinj  37956  0idl  38088  0rngo  38090  sticksstones11  42272  0prjspnlem  42744  0prjspnrel  42748  fvilbdRP  43810  frege54cor1c  44035  binomcxplemnotnn0  44476  snsslVD  44948  snssl  44949  unipwrVD  44951  unipwr  44952  sucidALTVD  44989  sucidALT  44990  sucidVD  44991  unisnALT  45045  nregmodel  45137  eliuniincex  45233  cnrefiisplem  45954  0cnf  46002  qndenserrnbl  46420  nnfoctbdjlem  46580  isomenndlem  46655  hoidmvlelem2  46721  hoiqssbl  46750  tannpoly  47017  sinnpoly  47018  funressnfv  47170  el1fzopredsuc  47452  setsidel  47503  sbgoldbo  47914  lincval0  48543  lcoel0  48556  1arympt1  48766  discsubc  49192  setc1onsubc  49730  initocmd  49797