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

Theorem elsncg 3919
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 2449 . 2  |-  ( x  =  A  ->  (
x  =  B  <->  A  =  B ) )
2 df-sn 3897 . 2  |-  { B }  =  { x  |  x  =  B }
31, 2elab2g 3127 1  |-  ( A  e.  V  ->  ( A  e.  { B } 
<->  A  =  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369    e. wcel 1756   {csn 3896
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-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 2577  df-v 2993  df-sn 3897
This theorem is referenced by:  elsnc  3920  elsni  3921  snidg  3922  eltpg  3937  eldifsn  4019  elsucg  4805  ltxr  11114  elfzp12  11558  ramcl  14109  pmtrdifellem4  16004  nbcusgra  23390  xrge0tsmsbi  26273  elzrhunit  26427  elzdif0  26428  plymulx  26968  frgrancvvdeqlem1  30646  bj-projval  32512
  Copyright terms: Public domain W3C validator