Theorem snid 4619

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  {csn 4580

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-sn 4581

This theorem is referenced by:  vsnid  4620  rabsnt  4688  sseliALT  5254  0sn0ep  5528  opthprc  5688  dmsnsnsn  6178  snsn0non  6443  fvrn0  6862  fsn  7080  fsn2  7081  fnsnbOLD  7112  fmptsng  7114  fmptsnd  7115  fvsng  7126  ovima0  7537  brtpos0  8175  tfrlem11  8319  mapsncnv  8831  0elixp  8867  domunsncan  9005  enfixsn  9014  infeq5i  9545  tc2  9649  djulcl  9822  djurcl  9823  djulf1o  9824  djuun  9838  isfin4p1  10225  fin1a2lem12  10321  dcomex  10357  axdc3lem4  10363  zornn0g  10415  axpowndlem3  10510  canthp1lem2  10564  elreal2  11043  xrinfmss  13225  fseq1p1m1  13514  1exp  14014  wrdexb  14448  divalgmod  16333  0bits  16366  lcmfunsnlem2  16567  0ram  16948  setsid  17134  imasvscafn  17458  imasvscaval  17459  gsumval2  18611  0subm  18742  gsumz  18761  smndex1mnd  18835  smndex1id  18836  mulgfval  18999  psgnsn  19449  psgnprfval2  19452  c0snmhm  20399  pzriprnglem4  21439  pzriprnglem5  21440  pzriprnglem7  21442  pzriprnglem9  21444  pzriprnglem13  21448  pzriprnglem14  21449  pzriprng1ALT  21451  mat0dimscm  22413  mat0scmat  22482  mvmumamul1  22498  m1detdiag  22541  pmatcoe1fsupp  22645  d0mat2pmat  22682  pmatcollpw3fi1lem1  22730  pmatcollpw3fi1lem2  22731  chpmat0d  22778  dfac14  23562  filconn  23827  uffix  23865  cnextfvval  24009  cnextcn  24011  ust0  24164  bndth  24913  ehl1eudis  25376  minveclem4a  25386  dvef  25940  tdeglem2  26022  mdegcl  26030  aalioulem2  26297  cxplogb  26752  xrlimcnp  26934  gausslemma2dlem4  27336  cofcutr  27920  cofcutrtime  27923  addsproplem4  27968  addsproplem5  27969  addsproplem6  27970  addsuniflem  27997  negsproplem4  28027  negsproplem5  28028  negsproplem6  28029  mulsproplem12  28123  sltmuls1  28143  sltmuls2  28144  mulsuniflem  28145  precsexlem11  28213  twocut  28419  pw2cut2  28458  axlowdimlem8  29022  axlowdimlem11  29025  upgr1e  29186  uspgr1e  29317  wlkl1loop  29711  wlk1walk  29712  wlk2v2elem1  30230  frgrncvvdeqlem7  30380  hsn0elch  31323  rabsnel  32575  aciunf1lem  32740  gsumwrd2dccatlem  33159  cyc2fv1  33203  1arithidom  33618  ply1dg1rtn0  33662  vieta  33736  lvecdim0  33763  lvecendof1f1o  33790  repr0  34768  bnj97  35022  bnj553  35054  bnj966  35100  bnj1442  35205  fineqvinfep  35281  subfacp1lem2a  35374  subfacp1lem5  35378  cvmliftlem4  35482  fmla0xp  35577  prv1n  35625  bj-0eltag  37179  poimirlem3  37824  poimirlem9  37830  poimirlem31  37852  poimirlem32  37853  prdsbnd  37994  heiborlem3  38014  grposnOLD  38083  grpokerinj  38094  0idl  38226  0rngo  38228  sticksstones11  42410  0prjspnlem  42866  0prjspnrel  42870  fvilbdRP  43931  frege54cor1c  44156  binomcxplemnotnn0  44597  snsslVD  45069  snssl  45070  unipwrVD  45072  unipwr  45073  sucidALTVD  45110  sucidALT  45111  sucidVD  45112  unisnALT  45166  nregmodel  45258  eliuniincex  45353  cnrefiisplem  46073  0cnf  46121  qndenserrnbl  46539  nnfoctbdjlem  46699  isomenndlem  46774  hoidmvlelem2  46840  hoiqssbl  46869  tannpoly  47136  sinnpoly  47137  funressnfv  47289  el1fzopredsuc  47571  setsidel  47622  sbgoldbo  48033  lincval0  48661  lcoel0  48674  1arympt1  48884  discsubc  49309  setc1onsubc  49847  initocmd  49914