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

Theorem elsnc2 4002
Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. This variation requires only that  B, rather than  A, be a set. (Contributed by NM, 12-Jun-1994.)
Hypothesis
Ref Expression
elsnc2.1  |-  B  e. 
_V
Assertion
Ref Expression
elsnc2  |-  ( A  e.  { B }  <->  A  =  B )

Proof of Theorem elsnc2
StepHypRef Expression
1 elsnc2.1 . 2  |-  B  e. 
_V
2 elsnc2g 4001 . 2  |-  ( B  e.  _V  ->  ( A  e.  { B } 
<->  A  =  B ) )
31, 2ax-mp 5 1  |-  ( A  e.  { B }  <->  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1405    e. wcel 1842   _Vcvv 3058   {csn 3971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3060  df-sn 3972
This theorem is referenced by:  fparlem1  6883  fparlem2  6884  el1o  7185  fin1a2lem11  8821  fin1a2lem12  8822  elnn0  10837  elfzp1  11783  fsumss  13694  fprodss  13905  elhoma  15633  islpidl  18212  zrhrhmb  18846  rest0  19961  qustgphaus  20911  taylfval  23044  elch0  26572  atoml2i  27701  bj-eltag  31087  dibopelvalN  34143  dibopelval2  34145  climrec  36958
  Copyright terms: Public domain W3C validator