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

Theorem snidg 3900
Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 28-Oct-2003.)
Assertion
Ref Expression
snidg  |-  ( A  e.  V  ->  A  e.  { A } )

Proof of Theorem snidg
StepHypRef Expression
1 eqid 2441 . 2  |-  A  =  A
2 elsncg 3897 . 2  |-  ( A  e.  V  ->  ( A  e.  { A } 
<->  A  =  A ) )
31, 2mpbiri 233 1  |-  ( A  e.  V  ->  A  e.  { A } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364    e. wcel 1761   {csn 3874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-sn 3875
This theorem is referenced by:  snidb  3901  elsnc2g  3904  snnzg  3989  fvunsn  5907  fsnunfv  5915  1stconst  6660  2ndconst  6661  curry1  6663  curry2  6666  suppsnop  6703  en1uniel  7377  unifpw  7610  sucprcreg  7810  mapfienOLD  7923  cfsuc  8422  elfzomin  11603  eqs1  12296  swrds1  12341  ramub1lem1  14083  acsfiindd  15343  odf1o1  16064  gsumconst  16419  lspsolv  17202  mavmul0  18322  mdetrlin  18368  mdetrsca  18369  maxlp  18710  cnpdis  18856  concompid  18994  dislly  19060  dfac14lem  19149  txtube  19172  pt1hmeo  19338  ufileu  19451  filufint  19452  uffix  19453  uffixsn  19457  i1fima2sn  21117  ply1rem  21594  1conngra  23496  vdgr1d  23508  vdgr1a  23511  eupap1  23532  esumel  26437  derangsn  26988  erdszelem4  27012  cvmlift2lem9  27130  locfindis  28502  neibastop2lem  28506  ismrer1  28662  kelac2  29343  rngunsnply  29455  eldmressnsn  29954  funressnfv  29959  fvressn  30077  hashrabsn1  30158  m1detdiag  30775  snlindsntor  30846  mnd1  30862  grp1  30863  lmod1lem1  30870  lmod1lem2  30871  lmod1lem3  30872  lmod1lem4  30873  lmod1lem5  30874  lmod1zr  30876  bj-sels  32185  elpaddatriN  33169
  Copyright terms: Public domain W3C validator