Theorem snid 4467

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

Syntax hints:   ∈ wcel 2048  Vcvv 3409  {csn 4435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-v 3411  df-sn 4436

This theorem is referenced by:  vsnid  4468  rabsnt  4535  sseliALT  5064  elALT  5184  intid  5200  0sn0ep  5315  opthprc  5459  dmsnsnsn  5910  snsn0non  6141  fvrn0  6521  fsn  6714  fsn2  6715  fnsnb  6745  fmptsng  6747  fmptsnd  6748  fvsng  6759  fvsnOLD  6761  fvsnun1OLD  6765  ovima0  7137  brtpos0  7695  tfrlem11  7821  mapsncnv  8247  0elixp  8282  domunsncan  8405  enfixsn  8414  infeq5i  8885  tc2  8970  djulcl  9125  djurcl  9126  djulf1o  9127  djuun  9141  isfin4p1  9527  fin1a2lem12  9623  dcomex  9659  axdc3lem4  9665  zornn0g  9717  axpowndlem3  9811  canthp1lem2  9865  elreal2  10344  xrinfmss  12512  fseq1p1m1  12790  1exp  13266  wrdexb  13674  divalgmod  15607  0bits  15638  lcmfunsnlem2  15830  0ram  16202  setsid  16384  imasvscafn  16656  imasvscaval  16657  xpsc0  16679  xpsc1  16680  gsumval2  17738  gsumz  17832  mulgfval  18003  psgnsn  18400  psgnprfval2  18403  mat0dimscm  20772  mat0scmat  20841  mvmumamul1  20857  m1detdiag  20900  pmatcoe1fsupp  21003  d0mat2pmat  21040  pmatcollpw3fi1lem1  21088  pmatcollpw3fi1lem2  21089  chpmat0d  21136  dfac14  21920  filconn  22185  uffix  22223  cnextfvval  22367  cnextcn  22369  ust0  22521  bndth  23255  ehl1eudis  23716  minveclem4a  23726  dvef  24270  tdeglem2  24348  mdegcl  24356  aalioulem2  24615  cxplogb  25055  xrlimcnp  25238  gausslemma2dlem4  25637  axlowdimlem8  26428  axlowdimlem11  26431  upgr1e  26591  uspgr1e  26719  wlkl1loop  27112  wlk1walk  27113  wlk2v2elem1  27674  frgrncvvdeqlem7  27829  hsn0elch  28794  rabsnel  30032  aciunf1lem  30159  lvecdim0  30590  signstfvn  31446  repr0  31491  bnj97  31746  bnj553  31778  bnj966  31824  bnj1442  31927  subfacp1lem2a  31972  subfacp1lem5  31976  cvmliftlem4  32080  bj-0eltag  33743  poimirlem3  34284  poimirlem9  34290  poimirlem31  34312  poimirlem32  34313  prdsbnd  34461  heiborlem3  34481  grposnOLD  34550  grpokerinj  34561  0idl  34693  0rngo  34695  0prjspnlem  38620  0prjspnrel  38621  fvilbdRP  39343  frege54cor1c  39569  binomcxplemnotnn0  40048  snsslVD  40526  snssl  40527  unipwrVD  40529  unipwr  40530  sucidALTVD  40567  sucidALT  40568  sucidVD  40569  unisnALT  40623  eliuniincex  40744  cnrefiisplem  41487  0cnf  41536  dvmptfprod  41606  qndenserrnbl  41957  nnfoctbdjlem  42114  isomenndlem  42189  hoidmvlelem2  42255  hoiqssbl  42284  funressnfv  42629  el1fzopredsuc  42877  setsidel  42888  sbgoldbo  43260  c0snmhm  43490  lincval0  43777  lcoel0  43790