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

Theorem elsncg 3738
Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15 (generalized). (Contributed by NM, 13-Sep-1995.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Assertion
Ref Expression
elsncg  |-  ( A  e.  V  ->  ( A  e.  { B } 
<->  A  =  B ) )

Proof of Theorem elsncg
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eqeq1 2364 . 2  |-  ( x  =  A  ->  (
x  =  B  <->  A  =  B ) )
2 df-sn 3722 . 2  |-  { B }  =  { x  |  x  =  B }
31, 2elab2g 2992 1  |-  ( A  e.  V  ->  ( A  e.  { B } 
<->  A  =  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1642    e. wcel 1710   {csn 3716
This theorem is referenced by:  elsnc  3739  elsni  3740  snidg  3741  eltpg  3752  eldifsn  3825  elsucg  4541  ltxr  10549  elfzp12  10953  ramcl  13173  xrge0tsmsbi  23416  elzrhunit  23636  elzdif0  23637  itgaddnclem2  25499  nbcusgra  27626  frgrancvvdeqlem1  27863
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-sn 3722
  Copyright terms: Public domain W3C validator