Theorem snid 4594

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-sn 4559

This theorem is referenced by:  vsnid  4595  rabsnt  4664  sseliALT  5228  elALT  5352  intid  5367  0sn0ep  5490  opthprc  5642  dmsnsnsn  6112  snsn0non  6370  fvrn0  6784  fsn  6989  fsn2  6990  fnsnb  7020  fmptsng  7022  fmptsnd  7023  fvsng  7034  ovima0  7429  brtpos0  8020  tfrlem11  8190  mapsncnv  8639  0elixp  8675  domunsncan  8812  enfixsn  8821  infeq5i  9324  tc2  9431  djulcl  9599  djurcl  9600  djulf1o  9601  djuun  9615  isfin4p1  10002  fin1a2lem12  10098  dcomex  10134  axdc3lem4  10140  zornn0g  10192  axpowndlem3  10286  canthp1lem2  10340  elreal2  10819  xrinfmss  12973  fseq1p1m1  13259  1exp  13740  wrdexb  14156  divalgmod  16043  0bits  16074  lcmfunsnlem2  16273  0ram  16649  setsid  16837  imasvscafn  17165  imasvscaval  17166  gsumval2  18285  0subm  18371  gsumz  18389  smndex1mnd  18464  smndex1id  18465  mulgfval  18617  psgnsn  19043  psgnprfval2  19046  mat0dimscm  21526  mat0scmat  21595  mvmumamul1  21611  m1detdiag  21654  pmatcoe1fsupp  21758  d0mat2pmat  21795  pmatcollpw3fi1lem1  21843  pmatcollpw3fi1lem2  21844  chpmat0d  21891  dfac14  22677  filconn  22942  uffix  22980  cnextfvval  23124  cnextcn  23126  ust0  23279  bndth  24027  ehl1eudis  24489  minveclem4a  24499  dvef  25049  tdeglem2  25131  mdegcl  25139  aalioulem2  25398  cxplogb  25841  xrlimcnp  26023  gausslemma2dlem4  26422  axlowdimlem8  27220  axlowdimlem11  27223  upgr1e  27386  uspgr1e  27514  wlkl1loop  27907  wlk1walk  27908  wlk2v2elem1  28420  frgrncvvdeqlem7  28570  hsn0elch  29511  rabsnel  30748  aciunf1lem  30901  cyc2fv1  31290  lvecdim0  31592  repr0  32491  bnj97  32746  bnj553  32778  bnj966  32824  bnj1442  32929  subfacp1lem2a  33042  subfacp1lem5  33046  cvmliftlem4  33150  fmla0xp  33245  prv1n  33293  cofcutr  34019  cofcutrtime  34020  bj-0eltag  35095  poimirlem3  35707  poimirlem9  35713  poimirlem31  35735  poimirlem32  35736  prdsbnd  35878  heiborlem3  35898  grposnOLD  35967  grpokerinj  35978  0idl  36110  0rngo  36112  sticksstones11  40040  0prjspnlem  40381  0prjspnrel  40385  fvilbdRP  41187  frege54cor1c  41412  binomcxplemnotnn0  41863  snsslVD  42338  snssl  42339  unipwrVD  42341  unipwr  42342  sucidALTVD  42379  sucidALT  42380  sucidVD  42381  unisnALT  42435  eliuniincex  42548  cnrefiisplem  43260  0cnf  43308  dvmptfprod  43376  qndenserrnbl  43726  nnfoctbdjlem  43883  isomenndlem  43958  hoidmvlelem2  44024  hoiqssbl  44053  funressnfv  44424  el1fzopredsuc  44705  setsidel  44716  sbgoldbo  45127  c0snmhm  45361  lincval0  45644  lcoel0  45657  1arympt1  45872