Theorem snid 4665

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-sn 4630

This theorem is referenced by:  vsnid  4666  rabsnt  4736  sseliALT  5310  intidOLD  5459  0sn0ep  5585  opthprc  5741  dmsnsnsn  6220  snsn0non  6490  fvrn0  6922  fsn  7133  fsn2  7134  fnsnb  7164  fmptsng  7166  fmptsnd  7167  fvsng  7178  ovima0  7586  brtpos0  8218  tfrlem11  8388  mapsncnv  8887  0elixp  8923  domunsncan  9072  enfixsn  9081  infeq5i  9631  tc2  9737  djulcl  9905  djurcl  9906  djulf1o  9907  djuun  9921  isfin4p1  10310  fin1a2lem12  10406  dcomex  10442  axdc3lem4  10448  zornn0g  10500  axpowndlem3  10594  canthp1lem2  10648  elreal2  11127  xrinfmss  13289  fseq1p1m1  13575  1exp  14057  wrdexb  14475  divalgmod  16349  0bits  16380  lcmfunsnlem2  16577  0ram  16953  setsid  17141  imasvscafn  17483  imasvscaval  17484  gsumval2  18605  0subm  18698  gsumz  18717  smndex1mnd  18791  smndex1id  18792  mulgfval  18952  psgnsn  19388  psgnprfval2  19391  mat0dimscm  21971  mat0scmat  22040  mvmumamul1  22056  m1detdiag  22099  pmatcoe1fsupp  22203  d0mat2pmat  22240  pmatcollpw3fi1lem1  22288  pmatcollpw3fi1lem2  22289  chpmat0d  22336  dfac14  23122  filconn  23387  uffix  23425  cnextfvval  23569  cnextcn  23571  ust0  23724  bndth  24474  ehl1eudis  24937  minveclem4a  24947  dvef  25497  tdeglem2  25579  mdegcl  25587  aalioulem2  25846  cxplogb  26291  xrlimcnp  26473  gausslemma2dlem4  26872  cofcutr  27411  cofcutrtime  27414  addsproplem4  27456  addsproplem5  27457  addsproplem6  27458  addsuniflem  27484  negsproplem4  27505  negsproplem5  27506  negsproplem6  27507  mulsproplem12  27583  ssltmul1  27602  ssltmul2  27603  mulsuniflem  27604  precsexlem11  27663  axlowdimlem8  28207  axlowdimlem11  28210  upgr1e  28373  uspgr1e  28501  wlkl1loop  28895  wlk1walk  28896  wlk2v2elem1  29408  frgrncvvdeqlem7  29558  hsn0elch  30501  rabsnel  31740  aciunf1lem  31887  cyc2fv1  32280  lvecdim0  32691  repr0  33623  bnj97  33877  bnj553  33909  bnj966  33955  bnj1442  34060  subfacp1lem2a  34171  subfacp1lem5  34175  cvmliftlem4  34279  fmla0xp  34374  prv1n  34422  bj-0eltag  35859  poimirlem3  36491  poimirlem9  36497  poimirlem31  36519  poimirlem32  36520  prdsbnd  36661  heiborlem3  36681  grposnOLD  36750  grpokerinj  36761  0idl  36893  0rngo  36895  sticksstones11  40972  0prjspnlem  41365  0prjspnrel  41369  fvilbdRP  42441  frege54cor1c  42666  binomcxplemnotnn0  43115  snsslVD  43590  snssl  43591  unipwrVD  43593  unipwr  43594  sucidALTVD  43631  sucidALT  43632  sucidVD  43633  unisnALT  43687  eliuniincex  43798  cnrefiisplem  44545  0cnf  44593  dvmptfprod  44661  qndenserrnbl  45011  nnfoctbdjlem  45171  isomenndlem  45246  hoidmvlelem2  45312  hoiqssbl  45341  funressnfv  45753  el1fzopredsuc  46033  setsidel  46044  sbgoldbo  46455  c0snmhm  46714  pzriprnglem4  46808  pzriprnglem5  46809  pzriprnglem7  46811  pzriprnglem9  46813  pzriprnglem13  46817  pzriprnglem14  46818  pzriprng1ALT  46820  lincval0  47096  lcoel0  47109  1arympt1  47324