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

Theorem snid 3908
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 3907 . 2  |-  ( A  e.  _V  <->  A  e.  { A } )
31, 2mpbi 208 1  |-  A  e. 
{ A }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   _Vcvv 2975   {csn 3880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-v 2977  df-sn 3881
This theorem is referenced by:  ssnid  3909  rabsnt  3955  sneqr  4043  sseliALT  4426  reusv6OLD  4506  elALT  4538  intid  4553  snsn0non  4840  opthprc  4889  dmsnsnsn  5320  fvrn0  5715  fsn  5884  fsn2  5886  fnsnb  5901  fmptsng  5903  fvsn  5914  fvsnun1  5916  ovima0  6245  brtpos0  6755  tfrlem11  6850  mapsn  7257  mapsncnv  7262  0elixp  7297  domunsncan  7414  enfixsn  7423  findcard2d  7557  infeq5i  7845  tc2  7965  isfin4-3  8487  fin1a2lem12  8583  dcomex  8619  axdc3lem4  8625  zornn0g  8677  axpowndlem3  8767  axpowndlem3OLD  8768  canthp1lem2  8823  elreal2  9302  xrinfmss  11275  fseq1p1m1  11537  1exp  11896  wrdexb  12248  0bits  13638  0ram  14084  setsid  14218  imasvscafn  14478  imasvscaval  14479  xpsc0  14501  xpsc1  14502  gsumz  15514  gsumval2  15516  psgnprfval2  16030  mvmumamul1  18368  maducoeval2  18449  dfac14  19194  filcon  19459  uffix  19497  cnextfvval  19640  cnextcn  19642  ust0  19797  bndth  20533  minveclem4a  20920  dvef  21455  tdeglem2  21533  mdegcl  21543  aalioulem2  21802  xrlimcnp  22365  axlowdimlem8  23198  axlowdimlem11  23201  vdgrf  23571  grposn  23705  rngosn  23894  hsn0elch  24654  rabsnel  25890  signstfvn  26973  subfacp1lem2a  27071  subfacp1lem5  27075  cvmliftlem4  27180  ghomsn  27310  prdsbnd  28695  heiborlem3  28715  grpokerinj  28753  0idl  28828  0rngo  28830  funressnfv  30037  frgrancvvdeqlem7  30632  frgrancvvdeqlemA  30633  fmptsnd  30725  psgnsn  30774  mat0dimscm  30868  pmatcoe1fsupp  30895  m1detdiag  30937  lincval0  30952  lcoel0  30965  snsslVD  31568  snssl  31569  unipwrVD  31571  unipwr  31572  sucidALTVD  31609  sucidALT  31610  sucidVD  31611  unisnALT  31665  bnj145OLD  31721  bnj97  31862  bnj553  31894  bnj966  31940  bnj1442  32043  bj-0eltag  32474
  Copyright terms: Public domain W3C validator