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

Theorem snid 3801
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 3800 . 2  |-  ( A  e.  _V  <->  A  e.  { A } )
31, 2mpbi 200 1  |-  A  e. 
{ A }
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   _Vcvv 2916   {csn 3774
This theorem is referenced by:  exsnrex  3808  rabsnt  3841  sneqr  3926  elALT  4367  rext  4372  unipw  4374  intid  4381  snsn0non  4659  snnex  4672  reusv6OLD  4693  opthprc  4884  dmsnsnsn  5307  fvrn0  5712  fsn  5865  fsn2  5867  fnressn  5877  fressnfv  5879  fvsn  5885  fvsnun1  5887  brtpos0  6445  opabiota  6497  tfrlem11  6608  mapsn  7014  mapsncnv  7019  0elixp  7052  domunsncan  7167  ac6sfi  7310  iunfi  7353  elirrv  7521  infeq5i  7547  tc2  7637  kmlem2  7987  isfin4-3  8151  fin1a2lem10  8245  fin1a2lem12  8247  hsmexlem4  8265  dcomex  8283  axdc3lem4  8289  zornn0g  8341  iunfo  8370  axpowndlem3  8430  canthp1lem2  8484  elreal2  8963  xrinfmss  10844  fseq1p1m1  11077  1exp  11364  wrdexb  11718  fsumcom2  12513  0bits  12906  0ram  13343  setsid  13463  imasvscafn  13717  imasvscaval  13718  xpsc0  13740  xpsc1  13741  gsumz  14736  gsumval2  14738  lbsextlem4  16188  dishaus  17400  dis2ndc  17476  dislly  17513  dfac14  17603  txdis  17617  txdis1cn  17620  txkgen  17637  filcon  17868  isufil2  17893  uffix  17906  alexsubALTlem4  18034  cnextfvval  18049  cnextcn  18051  tmdgsum  18078  ust0  18202  dscopn  18574  bndth  18936  minveclem4a  19284  ovolfiniun  19350  volfiniun  19394  dvef  19817  tdeglem2  19937  mdegcl  19945  aalioulem2  20203  xrlimcnp  20760  jensen  20780  cusgrares  21434  uvtx01vtx  21454  vdgrf  21622  grposn  21756  rngosn  21945  hsn0elch  22703  subfacp1lem2a  24819  subfacp1lem5  24823  cvmliftlem4  24928  cvmlift2lem1  24942  ghomsn  25052  fprodcom2  25261  wfrlem14  25483  wfrlem16  25485  funpartlem  25695  axlowdimlem8  25792  axlowdimlem11  25795  mbfresfi  26152  comppfsc  26277  prdsbnd  26392  heiborlem3  26412  grpokerinj  26450  0idl  26525  0rngo  26527  mzpcompact2lem  26698  frlmlbs  27117  enfixsn  27125  funressnfv  27859  frgrancvvdeqlem3  28135  frgrancvvdeqlem4  28136  frgrancvvdeqlem7  28139  frgrancvvdeqlemA  28140  frgrawopreg1  28153  frgrawopreg2  28154  snsslVD  28650  snssl  28651  unipwrVD  28653  unipwr  28654  sucidALTVD  28691  sucidALT  28692  sucidVD  28693  unisnALT  28747  bnj145  28800  bnj97  28943  bnj553  28975  bnj966  29021  bnj1442  29124  bnj1498  29136  pclfinN  30382
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-sn 3780
  Copyright terms: Public domain W3C validator