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

Theorem elsnc2 3669
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 3668 . 2  |-  ( B  e.  _V  ->  ( A  e.  { B } 
<->  A  =  B ) )
31, 2ax-mp 8 1  |-  ( A  e.  { B }  <->  A  =  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    e. wcel 1684   _Vcvv 2788   {csn 3640
This theorem is referenced by:  fparlem1  6218  fparlem2  6219  el1o  6498  fin1a2lem11  8036  fin1a2lem12  8037  elnn0  9967  elfzp1  10836  fsumss  12198  elhoma  13864  islpidl  15998  zrhrhmb  16465  rest0  16900  divstgphaus  17805  taylfval  19738  elch0  21833  atoml2i  22963  climrec  27729  dibopelvalN  31333  dibopelval2  31335
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-sn 3646
  Copyright terms: Public domain W3C validator