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

Syntax hints:   ∈ wcel 2110  Vcvv 3494  {csn 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-sn 4561

This theorem is referenced by:  vsnid  4595  rabsnt  4660  sseliALT  5205  elALT  5326  intid  5342  0sn0ep  5464  opthprc  5610  dmsnsnsn  6071  snsn0non  6303  fvrn0  6692  fsn  6891  fsn2  6892  fnsnb  6922  fmptsng  6924  fmptsnd  6925  fvsng  6936  ovima0  7321  brtpos0  7893  tfrlem11  8018  mapsncnv  8451  0elixp  8487  domunsncan  8611  enfixsn  8620  infeq5i  9093  tc2  9178  djulcl  9333  djurcl  9334  djulf1o  9335  djuun  9349  isfin4p1  9731  fin1a2lem12  9827  dcomex  9863  axdc3lem4  9869  zornn0g  9921  axpowndlem3  10015  canthp1lem2  10069  elreal2  10548  xrinfmss  12697  fseq1p1m1  12975  1exp  13452  wrdexb  13867  divalgmod  15751  0bits  15782  lcmfunsnlem2  15978  0ram  16350  setsid  16532  imasvscafn  16804  imasvscaval  16805  gsumval2  17890  0subm  17976  gsumz  17994  smndex1mnd  18069  smndex1id  18070  mulgfval  18220  psgnsn  18642  psgnprfval2  18645  mat0dimscm  21072  mat0scmat  21141  mvmumamul1  21157  m1detdiag  21200  pmatcoe1fsupp  21303  d0mat2pmat  21340  pmatcollpw3fi1lem1  21388  pmatcollpw3fi1lem2  21389  chpmat0d  21436  dfac14  22220  filconn  22485  uffix  22523  cnextfvval  22667  cnextcn  22669  ust0  22822  bndth  23556  ehl1eudis  24017  minveclem4a  24027  dvef  24571  tdeglem2  24649  mdegcl  24657  aalioulem2  24916  cxplogb  25358  xrlimcnp  25540  gausslemma2dlem4  25939  axlowdimlem8  26729  axlowdimlem11  26732  upgr1e  26892  uspgr1e  27020  wlkl1loop  27413  wlk1walk  27414  wlk2v2elem1  27928  frgrncvvdeqlem7  28078  hsn0elch  29019  rabsnel  30257  aciunf1lem  30401  cyc2fv1  30758  lvecdim0  31000  repr0  31877  bnj97  32133  bnj553  32165  bnj966  32211  bnj1442  32316  subfacp1lem2a  32422  subfacp1lem5  32426  cvmliftlem4  32530  fmla0xp  32625  prv1n  32673  bj-0eltag  34285  poimirlem3  34889  poimirlem9  34895  poimirlem31  34917  poimirlem32  34918  prdsbnd  35065  heiborlem3  35085  grposnOLD  35154  grpokerinj  35165  0idl  35297  0rngo  35299  0prjspnlem  39261  0prjspnrel  39262  fvilbdRP  40028  frege54cor1c  40254  binomcxplemnotnn0  40681  snsslVD  41156  snssl  41157  unipwrVD  41159  unipwr  41160  sucidALTVD  41197  sucidALT  41198  sucidVD  41199  unisnALT  41253  eliuniincex  41368  cnrefiisplem  42103  0cnf  42153  dvmptfprod  42223  qndenserrnbl  42574  nnfoctbdjlem  42731  isomenndlem  42806  hoidmvlelem2  42872  hoiqssbl  42901  funressnfv  43272  el1fzopredsuc  43519  setsidel  43530  sbgoldbo  43946  c0snmhm  44180  lincval0  44464  lcoel0  44477