MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snid Unicode version

Theorem snid 3701
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
StepHypRef Expression
1 snid.1 . 2  |-  A  e. 
_V
2 snidb 3700 . 2  |-  ( A  e.  _V  <->  A  e.  { A } )
31, 2mpbi 199 1  |-  A  e. 
{ A }
Colors of variables: wff set class
Syntax hints:    e. wcel 1701   _Vcvv 2822   {csn 3674
This theorem is referenced by:  rabsnt  3738  sneqr  3817  elALT  4255  rext  4259  unipw  4261  intid  4268  snsn0non  4548  snnex  4561  reusv6OLD  4582  opthprc  4773  dmsnsnsn  5188  fvrn0  5588  fsn  5734  fsn2  5736  fnressn  5744  fressnfv  5746  fvsn  5752  fvsnun1  5754  brtpos0  6283  opabiota  6335  tfrlem11  6446  mapsn  6852  mapsncnv  6857  0elixp  6890  domunsncan  7005  ac6sfi  7146  iunfi  7189  elirrv  7356  infeq5i  7382  tc2  7472  dfac9  7807  kmlem2  7822  isfin4-3  7986  fin1a2lem10  8080  fin1a2lem12  8082  hsmexlem4  8100  dcomex  8118  axdc3lem4  8124  zornn0g  8177  iunfo  8206  axpowndlem3  8266  canthp1lem2  8320  elreal2  8799  xrinfmss  10675  fseq1p1m1  10904  1exp  11178  wrdexb  11496  fsumcom2  12284  0bits  12677  0ram  13114  setsid  13234  imasvscafn  13488  imasvscaval  13489  xpsc0  13511  xpsc1  13512  gsumz  14507  gsumval2  14509  islbs3  15957  lbsextlem4  15963  dishaus  17166  dis2ndc  17242  dislly  17279  dfac14  17368  txdis  17382  txdis1cn  17385  txkgen  17402  filcon  17630  isufil2  17655  uffix  17668  ufinffr  17676  alexsubALTlem4  17796  tmdgsum  17830  dscopn  18148  bndth  18509  minveclem4a  18847  ovolfiniun  18913  volfiniun  18957  i1fd  19089  dvef  19380  tdeglem2  19500  mdegcl  19508  aalioulem2  19766  xrlimcnp  20316  jensen  20336  grposn  20935  rngosn  21124  hsn0elch  21882  cnextfvval  23415  ust0  23432  subfacp1lem2a  23995  subfacp1lem5  23999  cvmliftlem4  24103  cvmlift2lem1  24117  ghomsn  24279  wfrlem14  24654  wfrlem16  24656  funpartlem  24866  axlowdimlem8  24963  axlowdimlem11  24966  onint1  25274  comppfsc  25456  prdsbnd  25665  heiborlem3  25685  grpokerinj  25723  0idl  25798  0rngo  25800  mzpcompact2lem  25977  uvcff  26388  frlmlbs  26397  enfixsn  26405  islindf4  26456  funressnfv  27141  uvtx01vtx  27415  vdgref  27565  frgrancvvdeqlem3  27624  frgrancvvdeqlem4  27625  frgrancvvdeqlem7  27628  frgrancvvdeqlemA  27629  snsslVD  28115  snssl  28116  unipwrVD  28119  unipwr  28120  sucidALTVD  28157  sucidALT  28158  sucidVD  28159  unisnALT  28213  bnj145  28266  bnj97  28409  bnj553  28441  bnj966  28487  bnj1442  28590  bnj1498  28602  pclfinN  29907
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-v 2824  df-sn 3680
  Copyright terms: Public domain W3C validator