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 2109  Vcvv 3438  {csn 4579

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-sn 4580

This theorem is referenced by:  vsnid  4617  rabsnt  4685  sseliALT  5251  intidOLD  5405  0sn0ep  5527  opthprc  5687  dmsnsnsn  6173  snsn0non  6437  fvrn0  6854  fsn  7073  fsn2  7074  fnsnbOLD  7106  fmptsng  7108  fmptsnd  7109  fvsng  7120  ovima0  7532  brtpos0  8173  tfrlem11  8317  mapsncnv  8827  0elixp  8863  domunsncan  9001  enfixsn  9010  infeq5i  9551  tc2  9657  djulcl  9825  djurcl  9826  djulf1o  9827  djuun  9841  isfin4p1  10228  fin1a2lem12  10324  dcomex  10360  axdc3lem4  10366  zornn0g  10418  axpowndlem3  10512  canthp1lem2  10566  elreal2  11045  xrinfmss  13230  fseq1p1m1  13519  1exp  14016  wrdexb  14450  divalgmod  16335  0bits  16368  lcmfunsnlem2  16569  0ram  16950  setsid  17136  imasvscafn  17459  imasvscaval  17460  gsumval2  18578  0subm  18709  gsumz  18728  smndex1mnd  18802  smndex1id  18803  mulgfval  18966  psgnsn  19417  psgnprfval2  19420  c0snmhm  20366  pzriprnglem4  21409  pzriprnglem5  21410  pzriprnglem7  21412  pzriprnglem9  21414  pzriprnglem13  21418  pzriprnglem14  21419  pzriprng1ALT  21421  mat0dimscm  22372  mat0scmat  22441  mvmumamul1  22457  m1detdiag  22500  pmatcoe1fsupp  22604  d0mat2pmat  22641  pmatcollpw3fi1lem1  22689  pmatcollpw3fi1lem2  22690  chpmat0d  22737  dfac14  23521  filconn  23786  uffix  23824  cnextfvval  23968  cnextcn  23970  ust0  24123  bndth  24873  ehl1eudis  25336  minveclem4a  25346  dvef  25900  tdeglem2  25982  mdegcl  25990  aalioulem2  26257  cxplogb  26712  xrlimcnp  26894  gausslemma2dlem4  27296  cofcutr  27855  cofcutrtime  27858  addsproplem4  27902  addsproplem5  27903  addsproplem6  27904  addsuniflem  27931  negsproplem4  27960  negsproplem5  27961  negsproplem6  27962  mulsproplem12  28053  ssltmul1  28073  ssltmul2  28074  mulsuniflem  28075  precsexlem11  28142  twocut  28333  axlowdimlem8  28912  axlowdimlem11  28915  upgr1e  29076  uspgr1e  29207  wlkl1loop  29601  wlk1walk  29602  wlk2v2elem1  30117  frgrncvvdeqlem7  30267  hsn0elch  31210  rabsnel  32462  aciunf1lem  32619  gsumwrd2dccatlem  33032  cyc2fv1  33076  1arithidom  33487  ply1dg1rtn0  33528  lvecdim0  33581  lvecendof1f1o  33608  repr0  34581  bnj97  34835  bnj553  34867  bnj966  34913  bnj1442  35018  subfacp1lem2a  35155  subfacp1lem5  35159  cvmliftlem4  35263  fmla0xp  35358  prv1n  35406  bj-0eltag  36954  poimirlem3  37605  poimirlem9  37611  poimirlem31  37633  poimirlem32  37634  prdsbnd  37775  heiborlem3  37795  grposnOLD  37864  grpokerinj  37875  0idl  38007  0rngo  38009  sticksstones11  42132  0prjspnlem  42599  0prjspnrel  42603  fvilbdRP  43666  frege54cor1c  43891  binomcxplemnotnn0  44332  snsslVD  44805  snssl  44806  unipwrVD  44808  unipwr  44809  sucidALTVD  44846  sucidALT  44847  sucidVD  44848  unisnALT  44902  nregmodel  44994  eliuniincex  45090  cnrefiisplem  45814  0cnf  45862  qndenserrnbl  46280  nnfoctbdjlem  46440  isomenndlem  46515  hoidmvlelem2  46581  hoiqssbl  46610  tannpoly  46878  sinnpoly  46879  funressnfv  47031  el1fzopredsuc  47313  setsidel  47364  sbgoldbo  47775  lincval0  48404  lcoel0  48417  1arympt1  48627  discsubc  49053  setc1onsubc  49591  initocmd  49658