Theorem snid 4624

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

Syntax hints:   ∈ wcel 2145  Vcvv 3457  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-sn 4586

This theorem is referenced by:  vsnid  4625  rabsnt  4693  sseliALT  5263  0sn0ep  5555  opthprc  5715  dmsnsnsn  6210  snsn0non  6476  fvrn0  6899  fsn  7121  fsn2  7122  fnsnbOLD  7154  fmptsng  7156  fmptsnd  7157  fvsng  7168  ovima0  7579  brtpos0  8217  tfrlem11  8363  mapsncnv  8879  0elixp  8915  domunsncan  9053  enfixsn  9062  infeq5i  9593  tc2  9697  djulcl  9884  djurcl  9885  djulf1o  9886  djuun  9900  isfin4p1  10287  fin1a2lem12  10383  dcomex  10419  axdc3lem4  10425  zornn0g  10477  axpowndlem3  10572  canthp1lem2  10626  elreal2  11105  xrinfmss  13324  fseq1p1m1  13614  1exp  14115  wrdexb  14550  divalgmod  16452  0bits  16485  lcmfunsnlem2  16686  0ram  17068  setsid  17255  imasvscafn  17579  imasvscaval  17580  gsumval2  18732  0subm  18864  gsumz  18883  smndex1mnd  18960  smndex1id  18961  mulgfval  19123  psgnsn  19578  psgnprfval2  19581  c0snmhm  20533  pzriprnglem4  21591  pzriprnglem5  21592  pzriprnglem7  21594  pzriprnglem9  21596  pzriprnglem13  21600  pzriprnglem14  21601  pzriprng1ALT  21603  mat0dimscm  22583  mat0scmat  22652  mvmumamul1  22668  m1detdiag  22711  pmatcoe1fsupp  22815  d0mat2pmat  22852  pmatcollpw3fi1lem1  22900  pmatcollpw3fi1lem2  22901  chpmat0d  22948  dfac14  23732  filconn  23997  uffix  24035  cnextfvval  24179  cnextcn  24181  ust0  24334  bndth  25074  ehl1eudis  25536  minveclem4a  25546  dvef  26096  tdeglem2  26175  mdegcl  26183  aalioulem2  26451  cxplogb  26905  xrlimcnp  27087  gausslemma2dlem4  27487  cofcutr  28071  cofcutrtime  28074  addsproplem4  28119  addsproplem5  28120  addsproplem6  28121  addsuniflem  28148  negsproplem4  28178  negsproplem5  28179  negsproplem6  28180  mulsproplem12  28274  sltmuls1  28294  sltmuls2  28295  mulsuniflem  28296  precsexlem11  28364  twocut  28570  pw2cut2  28609  axlowdimlem8  29204  axlowdimlem11  29207  upgr1e  29368  uspgr1e  29499  wlkl1loop  29892  wlk1walk  29893  wlk2v2elem1  30411  frgrncvvdeqlem7  30561  hsn0elch  31505  rabsnel  32752  aciunf1lem  32915  gsumwrd2dccatlem  33305  cyc2fv1  33349  1arithidom  33739  ply1dg1rtn0  33783  0mplrim  33816  vieta  33882  lvecdim0  33909  lvecendof1f1o  33935  repr0  34910  bnj97  35166  bnj553  35198  bnj966  35244  bnj1442  35349  fineqvinfep  35428  subfacp1lem2a  35538  subfacp1lem5  35542  cvmliftlem4  35646  fmla0xp  35741  prv1n  35789  bj-0eltag  37470  poimirlem3  38129  poimirlem9  38135  poimirlem31  38157  poimirlem32  38158  prdsbnd  38299  heiborlem3  38319  grposnOLD  38388  grpokerinj  38399  0idl  38531  0rngo  38533  sticksstones11  42780  0prjspnlem  43212  0prjspnrel  43216  fvilbdRP  44273  frege54cor1c  44498  binomcxplemnotnn0  44925  snsslVD  45396  snssl  45397  unipwrVD  45399  unipwr  45400  sucidALTVD  45437  sucidALT  45438  sucidVD  45439  unisnALT  45493  nregmodel  45585  eliuniincex  45686  cnrefiisplem  46402  0cnf  46450  qndenserrnbl  46868  nnfoctbdjlem  47028  isomenndlem  47103  hoidmvlelem2  47169  hoiqssbl  47198  tannpoly  47483  sinnpoly  47484  funressnfv  47636  el1fzopredsuc  47919  setsidel  47981  sbgoldbo  48408  lincval0  49047  lcoel0  49060  1arympt1  49270  discsubc  49694  setc1onsubc  50232  initocmd  50299