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

Theorem elsncg 4052
 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

Proof of Theorem elsncg
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqeq1 2461 . 2
2 df-sn 4030 . 2
31, 2elab2g 3248 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  {csn 4029 This theorem is referenced by:  elsnc  4053  elsni  4054  snidg  4055  eltpg  4071  eldifsn  4155  elsucg  4950  ltxr  11353  elfzp12  11786  ramcl  14547  pmtrdifellem4  16504  nbcusgra  24463  frgrancvvdeqlem1  25030  xrge0tsmsbi  27776  elzrhunit  27960  elzdif0  27961  plymulx  28505  fprodn0f  31594  reclimc  31659  itgsincmulx  31773  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem53  31942  fourierdlem58  31947  fourierdlem60  31949  fourierdlem61  31950  fourierdlem62  31951  fourierdlem76  31965  fourierdlem101  31990  elaa2  32017  etransc  32066  initoeu2lem1  32620  bj-projval  34554 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-sn 4030
 Copyright terms: Public domain W3C validator