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

Theorem elsnc2 3573
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 3572 . 2  |-  ( B  e.  _V  ->  ( A  e.  { B } 
<->  A  =  B ) )
31, 2ax-mp 10 1  |-  ( A  e.  { B }  <->  A  =  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1619    e. wcel 1621   _Vcvv 2727   {csn 3544
This theorem is referenced by:  fparlem1  6070  fparlem2  6071  el1o  6384  fin1a2lem11  7920  fin1a2lem12  7921  elnn0  9846  elfzp1  10714  fsumss  12075  elhoma  13708  islpidl  15830  zrhrhmb  16297  rest0  16732  divstgphaus  17637  taylfval  19570  elch0  21663  atoml2i  22793  dibopelvalN  30022  dibopelval2  30024
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-sn 3550
  Copyright terms: Public domain W3C validator