Theorem elsncg 3993

Description: There is exactly 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 2457	. 2 |- ( x = A -> ( x = B <-> A = B ) )
2		df-sn 3971	. 2 |- { B } = { x | x = B }
3	1, 2	elab2g 3189	1 |- ( A e. V -> ( A e. { B } <-> A = B ) )

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1446   e. wcel 1889   {csn 3970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-sn 3971

This theorem is referenced by:  elsnc  3994  elsni  3995  snidg  3996  nelsn  4002  eltpg  4016  eldifsn  4100  elsucg  5493  ltxr  11422  elfzp12  11880  fprodn0f  14057  lcmfunsnlem2  14625  ramcl  14999  initoeu2lem1  15921  pmtrdifellem4  17132  logbmpt  23737  nbcusgra  25203  frgrancvvdeqlem1  25770  xrge0tsmsbi  28561  elzrhunit  28795  elzdif0  28796  esumrnmpt2  28901  plymulx  29449  bj-projval  31602  reclimc  37744  itgsincmulx  37861  dirkercncflem2  37976  dirkercncflem4  37978  fourierdlem53  38033  fourierdlem58  38038  fourierdlem60  38040  fourierdlem61  38041  fourierdlem62  38042  fourierdlem76  38056  fourierdlem101  38081  elaa2  38109  etransc  38159  qndenserrnbl  38174  sge0tsms  38232  sge0fodjrnlem  38268  el1fzopredsuc  38732