Theorem snid 4626

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-sn 4590

This theorem is referenced by:  vsnid  4627  rabsnt  4695  sseliALT  5264  intidOLD  5418  0sn0ep  5542  opthprc  5702  dmsnsnsn  6193  snsn0non  6459  fvrn0  6888  fsn  7107  fsn2  7108  fnsnbOLD  7140  fmptsng  7142  fmptsnd  7143  fvsng  7154  ovima0  7568  brtpos0  8212  tfrlem11  8356  mapsncnv  8866  0elixp  8902  domunsncan  9041  enfixsn  9050  infeq5i  9589  tc2  9695  djulcl  9863  djurcl  9864  djulf1o  9865  djuun  9879  isfin4p1  10268  fin1a2lem12  10364  dcomex  10400  axdc3lem4  10406  zornn0g  10458  axpowndlem3  10552  canthp1lem2  10606  elreal2  11085  xrinfmss  13270  fseq1p1m1  13559  1exp  14056  wrdexb  14490  divalgmod  16376  0bits  16409  lcmfunsnlem2  16610  0ram  16991  setsid  17177  imasvscafn  17500  imasvscaval  17501  gsumval2  18613  0subm  18744  gsumz  18763  smndex1mnd  18837  smndex1id  18838  mulgfval  19001  psgnsn  19450  psgnprfval2  19453  c0snmhm  20372  pzriprnglem4  21394  pzriprnglem5  21395  pzriprnglem7  21397  pzriprnglem9  21399  pzriprnglem13  21403  pzriprnglem14  21404  pzriprng1ALT  21406  mat0dimscm  22356  mat0scmat  22425  mvmumamul1  22441  m1detdiag  22484  pmatcoe1fsupp  22588  d0mat2pmat  22625  pmatcollpw3fi1lem1  22673  pmatcollpw3fi1lem2  22674  chpmat0d  22721  dfac14  23505  filconn  23770  uffix  23808  cnextfvval  23952  cnextcn  23954  ust0  24107  bndth  24857  ehl1eudis  25320  minveclem4a  25330  dvef  25884  tdeglem2  25966  mdegcl  25974  aalioulem2  26241  cxplogb  26696  xrlimcnp  26878  gausslemma2dlem4  27280  cofcutr  27832  cofcutrtime  27835  addsproplem4  27879  addsproplem5  27880  addsproplem6  27881  addsuniflem  27908  negsproplem4  27937  negsproplem5  27938  negsproplem6  27939  mulsproplem12  28030  ssltmul1  28050  ssltmul2  28051  mulsuniflem  28052  precsexlem11  28119  twocut  28309  axlowdimlem8  28876  axlowdimlem11  28879  upgr1e  29040  uspgr1e  29171  wlkl1loop  29566  wlk1walk  29567  wlk2v2elem1  30084  frgrncvvdeqlem7  30234  hsn0elch  31177  rabsnel  32429  aciunf1lem  32586  gsumwrd2dccatlem  33006  cyc2fv1  33078  1arithidom  33508  ply1dg1rtn0  33549  lvecdim0  33602  lvecendof1f1o  33629  repr0  34602  bnj97  34856  bnj553  34888  bnj966  34934  bnj1442  35039  subfacp1lem2a  35167  subfacp1lem5  35171  cvmliftlem4  35275  fmla0xp  35370  prv1n  35418  bj-0eltag  36966  poimirlem3  37617  poimirlem9  37623  poimirlem31  37645  poimirlem32  37646  prdsbnd  37787  heiborlem3  37807  grposnOLD  37876  grpokerinj  37887  0idl  38019  0rngo  38021  sticksstones11  42144  0prjspnlem  42611  0prjspnrel  42615  fvilbdRP  43679  frege54cor1c  43904  binomcxplemnotnn0  44345  snsslVD  44818  snssl  44819  unipwrVD  44821  unipwr  44822  sucidALTVD  44859  sucidALT  44860  sucidVD  44861  unisnALT  44915  nregmodel  45007  eliuniincex  45103  cnrefiisplem  45827  0cnf  45875  qndenserrnbl  46293  nnfoctbdjlem  46453  isomenndlem  46528  hoidmvlelem2  46594  hoiqssbl  46623  tannpoly  46891  sinnpoly  46892  funressnfv  47044  el1fzopredsuc  47326  setsidel  47377  sbgoldbo  47788  lincval0  48404  lcoel0  48417  1arympt1  48627  discsubc  49053  setc1onsubc  49591  initocmd  49658