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.

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

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