Theorem snid 4563

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

Syntax hints:   ∈ wcel 2112  Vcvv 3398  {csn 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-sn 4528

This theorem is referenced by:  vsnid  4564  rabsnt  4633  sseliALT  5187  elALT  5312  intid  5327  0sn0ep  5449  opthprc  5598  dmsnsnsn  6063  snsn0non  6310  fvrn0  6723  fsn  6928  fsn2  6929  fnsnb  6959  fmptsng  6961  fmptsnd  6962  fvsng  6973  ovima0  7365  brtpos0  7953  tfrlem11  8102  mapsncnv  8552  0elixp  8588  domunsncan  8723  enfixsn  8732  infeq5i  9229  tc2  9336  djulcl  9491  djurcl  9492  djulf1o  9493  djuun  9507  isfin4p1  9894  fin1a2lem12  9990  dcomex  10026  axdc3lem4  10032  zornn0g  10084  axpowndlem3  10178  canthp1lem2  10232  elreal2  10711  xrinfmss  12865  fseq1p1m1  13151  1exp  13629  wrdexb  14045  divalgmod  15930  0bits  15961  lcmfunsnlem2  16160  0ram  16536  setsid  16719  imasvscafn  16996  imasvscaval  16997  gsumval2  18112  0subm  18198  gsumz  18216  smndex1mnd  18291  smndex1id  18292  mulgfval  18444  psgnsn  18866  psgnprfval2  18869  mat0dimscm  21320  mat0scmat  21389  mvmumamul1  21405  m1detdiag  21448  pmatcoe1fsupp  21552  d0mat2pmat  21589  pmatcollpw3fi1lem1  21637  pmatcollpw3fi1lem2  21638  chpmat0d  21685  dfac14  22469  filconn  22734  uffix  22772  cnextfvval  22916  cnextcn  22918  ust0  23071  bndth  23809  ehl1eudis  24271  minveclem4a  24281  dvef  24831  tdeglem2  24913  mdegcl  24921  aalioulem2  25180  cxplogb  25623  xrlimcnp  25805  gausslemma2dlem4  26204  axlowdimlem8  26994  axlowdimlem11  26997  upgr1e  27158  uspgr1e  27286  wlkl1loop  27679  wlk1walk  27680  wlk2v2elem1  28192  frgrncvvdeqlem7  28342  hsn0elch  29283  rabsnel  30520  aciunf1lem  30673  cyc2fv1  31061  lvecdim0  31358  repr0  32257  bnj97  32513  bnj553  32545  bnj966  32591  bnj1442  32696  subfacp1lem2a  32809  subfacp1lem5  32813  cvmliftlem4  32917  fmla0xp  33012  prv1n  33060  cofcutr  33778  cofcutrtime  33779  bj-0eltag  34854  poimirlem3  35466  poimirlem9  35472  poimirlem31  35494  poimirlem32  35495  prdsbnd  35637  heiborlem3  35657  grposnOLD  35726  grpokerinj  35737  0idl  35869  0rngo  35871  sticksstones11  39781  0prjspnlem  40109  0prjspnrel  40113  fvilbdRP  40916  frege54cor1c  41141  binomcxplemnotnn0  41588  snsslVD  42063  snssl  42064  unipwrVD  42066  unipwr  42067  sucidALTVD  42104  sucidALT  42105  sucidVD  42106  unisnALT  42160  eliuniincex  42273  cnrefiisplem  42988  0cnf  43036  dvmptfprod  43104  qndenserrnbl  43454  nnfoctbdjlem  43611  isomenndlem  43686  hoidmvlelem2  43752  hoiqssbl  43781  funressnfv  44152  el1fzopredsuc  44433  setsidel  44444  sbgoldbo  44855  c0snmhm  45089  lincval0  45372  lcoel0  45385  1arympt1  45600