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 233	1 ⊢ 𝐴 ∈ {𝐴}

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-sn 4585

This theorem is used by:  vsnid  4620  rabsnt  4688  sseliALT  5262  0sn0ep  5554  opthprc  5714  dmsnsnsn  6221  snsn0non  6489  fvrn0  6914  fsn  7137  fsn2  7138  fnsnbOLD  7172  fmptsng  7174  fmptsnd  7175  fvsng  7186  ovima0  7601  brtpos0  8254  tfrlem11  8400  mapsncnv  8925  0elixp  8961  domunsncan  9100  enfixsn  9109  infeq5i  9641  tc2  9745  djulcl  9995  djurcl  9996  djulf1o  9997  djuun  10011  isfin4p1  10397  fin1a2lem12  10493  dcomex  10529  axdc3lem4  10535  zornn0g  10587  axpowndlem3  10688  canthp1lem2  10742  elreal2  11221  xrinfmss  13444  fseq1p1m1  13736  1exp  14238  wrdexb  14674  divalgmod  16582  0bits  16615  lcmfunsnlem2  16821  0ram  17204  setsid  17391  imasvscafn  17715  imasvscaval  17716  gsumval2  18881  0subm  19019  gsumz  19038  smndex1mnd  19115  smndex1id  19116  mulgfval  19285  psgnsn  19740  psgnprfval2  19743  c0snmhm  20699  pzriprnglem4  21796  pzriprnglem5  21797  pzriprnglem7  21799  pzriprnglem9  21801  pzriprnglem13  21805  pzriprnglem14  21806  pzriprng1ALT  21808  mat0dimscm  22790  mat0scmat  22859  mvmumamul1  22875  m1detdiag  22918  pmatcoe1fsupp  23025  d0mat2pmat  23062  pmatcollpw3fi1lem1  23110  pmatcollpw3fi1lem2  23111  chpmat0d  23158  dfac14  23943  filconn  24208  uffix  24246  cnextfvval  24390  cnextcn  24392  ust0  24545  bndth  25285  ehl1eudis  25747  minveclem4a  25757  dvef  26306  tdeglem2  26385  mdegcl  26393  aalioulem2  26666  cxplogb  27120  xrlimcnp  27302  gausslemma2dlem4  27702  cofcutr  28316  cofcutrtime  28319  addsproplem4  28364  addsproplem5  28365  addsproplem6  28366  addsuniflem  28393  negsproplem4  28423  negsproplem5  28424  negsproplem6  28425  mulsproplem12  28519  sltmuls1  28539  sltmuls2  28540  mulsuniflem  28541  precsexlem11  28609  twocut  28815  pw2cut2  28854  axlowdimlem8  29533  axlowdimlem11  29536  upgr1e  29697  uspgr1e  29831  wlkl1loop  30224  wlk1walk  30225  wlk2v2elem1  30762  frgrncvvdeqlem7  30912  hsn0elch  31856  rabsnel  33144  aciunf1lem  33304  gsumwrd2dccatlem  33685  cyc2fv1  33729  1arithidom  34116  ply1dg1rtn0  34160  0mplrim  34193  vieta  34259  lvecdim0  34286  lvecendof1f1o  34312  repr0  35287  bnj97  35543  bnj553  35575  bnj966  35621  bnj1442  35726  fineqvinfep  35850  subfacp1lem2a  36032  subfacp1lem5  36036  cvmliftlem4  36140  fmla0xp  36235  prv1n  36283  bj-0eltag  37984  poimirlem3  38635  poimirlem9  38641  poimirlem31  38663  poimirlem32  38664  prdsbnd  38821  heiborlem3  38841  grposnOLD  38910  grpokerinj  38921  0idl  39053  0rngo  39055  sticksstones11  43300  0prjspnlem  43756  0prjspnrel  43757  fvilbdRP  44784  frege54cor1c  45009  binomcxplemnotnn0  45434  snsslVD  45905  snssl  45906  unipwrVD  45908  unipwr  45909  sucidALTVD  45946  sucidALT  45947  sucidVD  45948  unisnALT  46002  nregmodel  46101  eliuniincex  46218  cnrefiisplem  46933  0cnf  46981  qndenserrnbl  47399  nnfoctbdjlem  47559  isomenndlem  47634  hoidmvlelem2  47700  hoiqssbl  47729  tannpoly  48034  sinnpoly  48035  funressnfv  48207  el1fzopredsuc  48490  setsidel  48552  sbgoldbo  48979  lincval0  49621  lcoel0  49634  1arympt1  49844  discsubc  50272  setc1onsubc  50834  parhomid2  50845  parhomid  50846  parcatid2  50857  parcatid  50858  initocmd  50946