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

Theorem elsnc2 3908
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 3907 . 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 1369    e. wcel 1756   _Vcvv 2972   {csn 3877
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 2568  df-v 2974  df-sn 3878
This theorem is referenced by:  fparlem1  6672  fparlem2  6673  el1o  6939  fin1a2lem11  8579  fin1a2lem12  8580  elnn0  10581  elfzp1  11505  fsumss  13202  elhoma  14900  islpidl  17328  zrhrhmb  17942  rest0  18773  divstgphaus  19693  taylfval  21824  elch0  24657  atoml2i  25787  fprodss  27461  climrec  29776  bj-eltag  32470  dibopelvalN  34788  dibopelval2  34790
  Copyright terms: Public domain W3C validator