Theorem snid 4614

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

Syntax hints:   ∈ wcel 2106  Vcvv 3442  {csn 4578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3444  df-sn 4579

This theorem is referenced by:  vsnid  4615  rabsnt  4684  sseliALT  5258  intidOLD  5408  0sn0ep  5533  opthprc  5687  dmsnsnsn  6163  snsn0non  6430  fvrn0  6860  fsn  7068  fsn2  7069  fnsnb  7099  fmptsng  7101  fmptsnd  7102  fvsng  7113  ovima0  7518  brtpos0  8124  tfrlem11  8294  mapsncnv  8757  0elixp  8793  domunsncan  8942  enfixsn  8951  infeq5i  9498  tc2  9604  djulcl  9772  djurcl  9773  djulf1o  9774  djuun  9788  isfin4p1  10177  fin1a2lem12  10273  dcomex  10309  axdc3lem4  10315  zornn0g  10367  axpowndlem3  10461  canthp1lem2  10515  elreal2  10994  xrinfmss  13150  fseq1p1m1  13436  1exp  13918  wrdexb  14333  divalgmod  16215  0bits  16246  lcmfunsnlem2  16443  0ram  16819  setsid  17007  imasvscafn  17346  imasvscaval  17347  gsumval2  18468  0subm  18554  gsumz  18572  smndex1mnd  18646  smndex1id  18647  mulgfval  18799  psgnsn  19225  psgnprfval2  19228  mat0dimscm  21724  mat0scmat  21793  mvmumamul1  21809  m1detdiag  21852  pmatcoe1fsupp  21956  d0mat2pmat  21993  pmatcollpw3fi1lem1  22041  pmatcollpw3fi1lem2  22042  chpmat0d  22089  dfac14  22875  filconn  23140  uffix  23178  cnextfvval  23322  cnextcn  23324  ust0  23477  bndth  24227  ehl1eudis  24690  minveclem4a  24700  dvef  25250  tdeglem2  25332  mdegcl  25340  aalioulem2  25599  cxplogb  26042  xrlimcnp  26224  gausslemma2dlem4  26623  axlowdimlem8  27606  axlowdimlem11  27609  upgr1e  27772  uspgr1e  27900  wlkl1loop  28294  wlk1walk  28295  wlk2v2elem1  28807  frgrncvvdeqlem7  28957  hsn0elch  29898  rabsnel  31134  aciunf1lem  31284  cyc2fv1  31673  lvecdim0  31986  repr0  32889  bnj97  33143  bnj553  33175  bnj966  33221  bnj1442  33326  subfacp1lem2a  33439  subfacp1lem5  33443  cvmliftlem4  33547  fmla0xp  33642  prv1n  33690  cofcutr  34200  cofcutrtime  34201  addsproplem4  34236  addsproplem5  34237  addsproplem6  34238  addsunif  34256  bj-0eltag  35303  poimirlem3  35934  poimirlem9  35940  poimirlem31  35962  poimirlem32  35963  prdsbnd  36105  heiborlem3  36125  grposnOLD  36194  grpokerinj  36205  0idl  36337  0rngo  36339  sticksstones11  40418  0prjspnlem  40771  0prjspnrel  40775  fvilbdRP  41669  frege54cor1c  41894  binomcxplemnotnn0  42345  snsslVD  42820  snssl  42821  unipwrVD  42823  unipwr  42824  sucidALTVD  42861  sucidALT  42862  sucidVD  42863  unisnALT  42917  eliuniincex  43029  cnrefiisplem  43756  0cnf  43804  dvmptfprod  43872  qndenserrnbl  44222  nnfoctbdjlem  44380  isomenndlem  44455  hoidmvlelem2  44521  hoiqssbl  44550  funressnfv  44953  el1fzopredsuc  45233  setsidel  45244  sbgoldbo  45655  c0snmhm  45889  lincval0  46172  lcoel0  46185  1arympt1  46400