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

Theorem elsnc2 3671
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 3670 . 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 1624    e. wcel 1685   _Vcvv 2790   {csn 3642
This theorem is referenced by:  fparlem1  6180  fparlem2  6181  el1o  6494  fin1a2lem11  8032  fin1a2lem12  8033  elnn0  9963  elfzp1  10831  fsumss  12193  elhoma  13859  islpidl  15993  zrhrhmb  16460  rest0  16895  divstgphaus  17800  taylfval  19733  elch0  21826  atoml2i  22956  climrec  27129  dibopelvalN  30601  dibopelval2  30603
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-sn 3648
  Copyright terms: Public domain W3C validator