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

Theorem elsnc2 4064
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 4063 . 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 1379    e. wcel 1767   _Vcvv 3118   {csn 4033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-sn 4034
This theorem is referenced by:  fparlem1  6895  fparlem2  6896  el1o  7161  fin1a2lem11  8802  fin1a2lem12  8803  elnn0  10809  elfzp1  11742  fsumss  13526  elhoma  15233  islpidl  17762  zrhrhmb  18415  rest0  19536  qustgphaus  20487  taylfval  22619  elch0  26003  atoml2i  27133  fprodss  29014  climrec  31474  bj-eltag  34022  dibopelvalN  36346  dibopelval2  36348
  Copyright terms: Public domain W3C validator