Theorem elsng 4586

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
elsng	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))

Proof of Theorem elsng

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2740	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵))
2		df-sn 4573	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
3	1, 2	elab2g 3621	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ∈ wcel 2105  {csn 4572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-sn 4573

This theorem is referenced by:  elsn  4587  elsni  4589  snidg  4606  eltpg  4632  eldifsn  4733  sneqrg  4783  elsucg  6363  ltxr  12944  elfzp12  13428  fprodn0f  15792  lcmfunsnlem2  16434  ramcl  16819  initoeu2lem1  17818  pmtrdifellem4  19175  logbmpt  26036  2lgslem2  26641  elunsn  31087  xrge0tsmsbi  31546  dimkerim  31947  elzrhunit  32168  esumrnmpt2  32275  plymulx  32768  bj-projval  35275  bj-elsn12g  35329  bj-elsnb  35330  bj-snmoore  35382  bj-elsn0  35424  eldmressnALTV  36530  brressn  36701  aks4d1p6  40336  sticksstones11  40362  metakunt20  40394  reclimc  43519  itgsincmulx  43840  dirkercncflem2  43970  dirkercncflem4  43972  fourierdlem53  44025  fourierdlem58  44030  fourierdlem60  44032  fourierdlem61  44033  fourierdlem62  44034  fourierdlem76  44048  fourierdlem101  44073  elaa2  44100  etransc  44149  qndenserrnbl  44161  sge0tsms  44244  el1fzopredsuc  45157  mndtcob  46709