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

Theorem snid 3667
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 3666 . 2  |-  ( A  e.  _V  <->  A  e.  { A } )
31, 2mpbi 199 1  |-  A  e. 
{ A }
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788   {csn 3640
This theorem is referenced by:  rabsnt  3704  sneqr  3780  elALT  4218  rext  4222  unipw  4224  intid  4231  snsn0non  4511  snnex  4524  reusv6OLD  4545  opthprc  4736  dmsnsnsn  5151  fvrn0  5550  fsn  5696  fsn2  5698  fnressn  5705  fressnfv  5707  fvsn  5713  fvsnun1  5715  brtpos0  6241  opabiota  6293  tfrlem11  6404  mapsn  6809  mapsncnv  6814  0elixp  6847  domunsncan  6962  ac6sfi  7101  iunfi  7144  elirrv  7311  infeq5i  7337  tc2  7427  dfac9  7762  kmlem2  7777  isfin4-3  7941  fin1a2lem10  8035  fin1a2lem12  8037  hsmexlem4  8055  dcomex  8073  axdc3lem4  8079  zornn0g  8132  iunfo  8161  axpowndlem3  8221  canthp1lem2  8275  elreal2  8754  xrinfmss  10628  fseq1p1m1  10857  1exp  11131  wrdexb  11449  fsumcom2  12237  0bits  12630  0ram  13067  setsid  13187  imasvscafn  13439  imasvscaval  13440  xpsc0  13462  xpsc1  13463  gsumz  14458  gsumval2  14460  islbs3  15908  lbsextlem4  15914  dishaus  17110  dis2ndc  17186  dislly  17223  dfac14  17312  txdis  17326  txdis1cn  17329  txkgen  17346  filcon  17578  isufil2  17603  uffix  17616  ufinffr  17624  alexsubALTlem4  17744  tmdgsum  17778  dscopn  18096  bndth  18456  minveclem4a  18794  ovolfiniun  18860  volfiniun  18904  i1fd  19036  dvef  19327  tdeglem2  19447  mdegcl  19455  aalioulem2  19713  xrlimcnp  20263  jensen  20283  grposn  20882  rngosn  21071  hsn0elch  21827  subfacp1lem2a  23711  subfacp1lem5  23715  cvmliftlem4  23819  cvmlift2lem1  23833  ghomsn  23995  wfrlem14  24269  wfrlem16  24271  funpartfv  24483  axlowdimlem8  24577  axlowdimlem11  24580  onint1  24888  limvinlv  25559  1ded  25738  comppfsc  26307  prdsbnd  26517  heiborlem3  26537  grpokerinj  26575  0idl  26650  0rngo  26652  mzpcompact2lem  26829  uvcff  27240  frlmlbs  27249  enfixsn  27257  islindf4  27308  funressnfv  27991  uvtx01vtx  28164  snsslVD  28604  snssl  28605  unipwrVD  28608  unipwr  28609  sucidALTVD  28646  sucidALT  28647  sucidVD  28648  unisnALT  28702  bnj145  28755  bnj97  28898  bnj553  28930  bnj966  28976  bnj1442  29079  bnj1498  29091  pclfinN  30089
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-sn 3646
  Copyright terms: Public domain W3C validator