Theorem snid 4208

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	|- A e. _V

Assertion

Ref	Expression
snid	|- A e. { A }

Proof of Theorem snid

Step	Hyp	Ref	Expression
1		snid.1	. 2 |- A e. _V
2		snidb 4207	. 2 |- ( A e. _V <-> A e. { A } )
3	1, 2	mpbi 220	1 |- A e. { A }

Syntax hints:   e. wcel 1990   _Vcvv 3200   {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-sn 4178

This theorem is referenced by:  vsnid  4209  rabsnt  4266  sseliALT  4791  elALT  4910  intid  4926  opthprc  5167  dmsnsnsn  5613  snsn0non  5846  fvrn0  6216  fsn  6402  fsn2  6403  fnsnb  6432  fmptsng  6434  fmptsnd  6435  fvsn  6446  fvsnun1  6448  ovima0  6813  brtpos0  7359  tfrlem11  7484  mapsn  7899  mapsncnv  7904  0elixp  7939  domunsncan  8060  enfixsn  8069  infeq5i  8533  tc2  8618  isfin4-3  9137  fin1a2lem12  9233  dcomex  9269  axdc3lem4  9275  zornn0g  9327  axpowndlem3  9421  canthp1lem2  9475  elreal2  9953  xrinfmss  12140  fseq1p1m1  12414  1exp  12889  wrdexb  13316  divalgmod  15129  0bits  15161  lcmfunsnlem2  15353  0ram  15724  setsid  15914  imasvscafn  16197  imasvscaval  16198  xpsc0  16220  xpsc1  16221  gsumval2  17280  gsumz  17374  psgnsn  17940  psgnprfval2  17943  mat0dimscm  20275  mat0scmat  20344  mvmumamul1  20360  m1detdiag  20403  pmatcoe1fsupp  20506  d0mat2pmat  20543  pmatcollpw3fi1lem1  20591  pmatcollpw3fi1lem2  20592  chpmat0d  20639  dfac14  21421  filconn  21687  uffix  21725  cnextfvval  21869  cnextcn  21871  ust0  22023  bndth  22757  minveclem4a  23201  dvef  23743  tdeglem2  23821  mdegcl  23829  aalioulem2  24088  cxplogb  24524  xrlimcnp  24695  gausslemma2dlem4  25094  axlowdimlem8  25829  axlowdimlem11  25832  upgr1e  26008  uspgr1e  26136  wlkl1loop  26534  wlk1walk  26535  wlk2v2elem1  27015  frgrncvvdeqlem7  27169  hsn0elch  28105  rabsnel  29341  aciunf1lem  29462  signstfvn  30646  repr0  30689  bnj145OLD  30795  bnj97  30936  bnj553  30968  bnj966  31014  bnj1442  31117  subfacp1lem2a  31162  subfacp1lem5  31166  cvmliftlem4  31270  bj-0eltag  32966  poimirlem3  33412  poimirlem9  33418  poimirlem31  33440  poimirlem32  33441  prdsbnd  33592  heiborlem3  33612  grposnOLD  33681  grpokerinj  33692  0idl  33824  0rngo  33826  fvilbdRP  37982  frege54cor1c  38209  binomcxplemnotnn0  38555  snsslVD  39064  snssl  39065  unipwrVD  39067  unipwr  39068  sucidALTVD  39106  sucidALT  39107  sucidVD  39108  unisnALT  39162  eliuniincex  39292  mapsnd  39388  cnrefiisplem  40055  0cnf  40090  dvmptfprod  40160  qndenserrnbl  40515  nnfoctbdjlem  40672  isomenndlem  40744  hoidmvlelem2  40810  hoiqssbl  40839  funressnfv  41208  el1fzopredsuc  41335  setsidel  41346  sbgoldbo  41675  c0snmhm  41915  lincval0  42204  lcoel0  42217