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.

Step	Hyp	Ref	Expression
1		eqeq1 2461	. 2
2		df-sn 4030	. 2
3	1, 2	elab2g 3248	1

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