Theorem snid 4615

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  {csn 4576

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-sn 4577

This theorem is referenced by:  vsnid  4616  rabsnt  4684  sseliALT  5247  0sn0ep  5520  opthprc  5680  dmsnsnsn  6167  snsn0non  6432  fvrn0  6850  fsn  7068  fsn2  7069  fnsnbOLD  7100  fmptsng  7102  fmptsnd  7103  fvsng  7114  ovima0  7525  brtpos0  8163  tfrlem11  8307  mapsncnv  8817  0elixp  8853  domunsncan  8990  enfixsn  8999  infeq5i  9526  tc2  9630  djulcl  9803  djurcl  9804  djulf1o  9805  djuun  9819  isfin4p1  10206  fin1a2lem12  10302  dcomex  10338  axdc3lem4  10344  zornn0g  10396  axpowndlem3  10490  canthp1lem2  10544  elreal2  11023  xrinfmss  13209  fseq1p1m1  13498  1exp  13998  wrdexb  14432  divalgmod  16317  0bits  16350  lcmfunsnlem2  16551  0ram  16932  setsid  17118  imasvscafn  17441  imasvscaval  17442  gsumval2  18594  0subm  18725  gsumz  18744  smndex1mnd  18818  smndex1id  18819  mulgfval  18982  psgnsn  19433  psgnprfval2  19436  c0snmhm  20382  pzriprnglem4  21422  pzriprnglem5  21423  pzriprnglem7  21425  pzriprnglem9  21427  pzriprnglem13  21431  pzriprnglem14  21432  pzriprng1ALT  21434  mat0dimscm  22385  mat0scmat  22454  mvmumamul1  22470  m1detdiag  22513  pmatcoe1fsupp  22617  d0mat2pmat  22654  pmatcollpw3fi1lem1  22702  pmatcollpw3fi1lem2  22703  chpmat0d  22750  dfac14  23534  filconn  23799  uffix  23837  cnextfvval  23981  cnextcn  23983  ust0  24136  bndth  24885  ehl1eudis  25348  minveclem4a  25358  dvef  25912  tdeglem2  25994  mdegcl  26002  aalioulem2  26269  cxplogb  26724  xrlimcnp  26906  gausslemma2dlem4  27308  cofcutr  27869  cofcutrtime  27872  addsproplem4  27916  addsproplem5  27917  addsproplem6  27918  addsuniflem  27945  negsproplem4  27974  negsproplem5  27975  negsproplem6  27976  mulsproplem12  28067  ssltmul1  28087  ssltmul2  28088  mulsuniflem  28089  precsexlem11  28156  twocut  28347  pw2cut2  28383  axlowdimlem8  28928  axlowdimlem11  28931  upgr1e  29092  uspgr1e  29223  wlkl1loop  29617  wlk1walk  29618  wlk2v2elem1  30133  frgrncvvdeqlem7  30283  hsn0elch  31226  rabsnel  32478  aciunf1lem  32642  gsumwrd2dccatlem  33044  cyc2fv1  33088  1arithidom  33500  ply1dg1rtn0  33542  lvecdim0  33617  lvecendof1f1o  33644  repr0  34622  bnj97  34876  bnj553  34908  bnj966  34954  bnj1442  35059  subfacp1lem2a  35222  subfacp1lem5  35226  cvmliftlem4  35330  fmla0xp  35425  prv1n  35473  bj-0eltag  37018  poimirlem3  37669  poimirlem9  37675  poimirlem31  37697  poimirlem32  37698  prdsbnd  37839  heiborlem3  37859  grposnOLD  37928  grpokerinj  37939  0idl  38071  0rngo  38073  sticksstones11  42195  0prjspnlem  42662  0prjspnrel  42666  fvilbdRP  43729  frege54cor1c  43954  binomcxplemnotnn0  44395  snsslVD  44867  snssl  44868  unipwrVD  44870  unipwr  44871  sucidALTVD  44908  sucidALT  44909  sucidVD  44910  unisnALT  44964  nregmodel  45056  eliuniincex  45152  cnrefiisplem  45873  0cnf  45921  qndenserrnbl  46339  nnfoctbdjlem  46499  isomenndlem  46574  hoidmvlelem2  46640  hoiqssbl  46669  tannpoly  46927  sinnpoly  46928  funressnfv  47080  el1fzopredsuc  47362  setsidel  47413  sbgoldbo  47824  lincval0  48453  lcoel0  48466  1arympt1  48676  discsubc  49102  setc1onsubc  49640  initocmd  49707