Theorem elsncg 3967

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.

Step	Hyp	Ref	Expression
1		eqeq1 2386	. 2 |- ( x = A -> ( x = B <-> A = B ) )
2		df-sn 3945	. 2 |- { B } = { x | x = B }
3	1, 2	elab2g 3173	1 |- ( A e. V -> ( A e. { B } <-> A = B ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1399   e. wcel 1826   {csn 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-sn 3945

This theorem is referenced by:  elsnc  3968  elsni  3969  snidg  3970  eltpg  3986  eldifsn  4069  elsucg  4859  ltxr  11245  elfzp12  11679  ramcl  14549  initoeu2lem1  15410  pmtrdifellem4  16621  logbmpt  23246  nbcusgra  24584  frgrancvvdeqlem1  25151  xrge0tsmsbi  27930  elzrhunit  28113  elzdif0  28114  esumrnmpt2  28216  plymulx  28688  fprodn0f  31760  reclimc  31825  itgsincmulx  31939  dirkercncflem2  32052  dirkercncflem4  32054  fourierdlem53  32108  fourierdlem58  32113  fourierdlem60  32115  fourierdlem61  32116  fourierdlem62  32117  fourierdlem76  32131  fourierdlem101  32156  elaa2  32183  etransc  32232  bj-projval  34902