Theorem elsng 4572

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 2742	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵))
2		df-sn 4559	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
3	1, 2	elab2g 3604	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-sn 4559

This theorem is referenced by:  elsn  4573  elsni  4575  snidg  4592  eltpg  4618  eldifsn  4717  sneqrg  4767  elsucg  6318  ltxr  12780  elfzp12  13264  fprodn0f  15629  lcmfunsnlem2  16273  ramcl  16658  initoeu2lem1  17645  pmtrdifellem4  19002  logbmpt  25843  2lgslem2  26448  elunsn  30759  xrge0tsmsbi  31220  dimkerim  31610  elzrhunit  31829  esumrnmpt2  31936  plymulx  32427  bj-projval  35113  bj-elsn12g  35158  bj-elsnb  35159  bj-snmoore  35211  bj-elsn0  35253  aks4d1p6  40017  sticksstones11  40040  metakunt20  40072  reclimc  43084  itgsincmulx  43405  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem53  43590  fourierdlem58  43595  fourierdlem60  43597  fourierdlem61  43598  fourierdlem62  43599  fourierdlem76  43613  fourierdlem101  43638  elaa2  43665  etransc  43714  qndenserrnbl  43726  sge0tsms  43808  el1fzopredsuc  44705  mndtcob  46255