Theorem elsng 4606

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {csn 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-sn 4593

This theorem is referenced by:  elsn  4607  elsni  4609  snidg  4627  elunsn  4650  eltpg  4653  el7g  4657  eldifsn  4753  sneqrg  4806  elsucg  6405  ltxr  13082  elfzp12  13571  fzdif1  13573  fprodn0f  15964  lcmfunsnlem2  16617  ramcl  17007  initoeu2lem1  17983  pmtrdifellem4  19416  psdmul  22060  logbmpt  26705  2lgslem2  27313  xrge0tsmsbi  33010  rprmnz  33498  dimkerim  33630  elzrhunit  33974  esumrnmpt2  34065  plymulx  34546  bj-projval  36991  bj-elsn12g  37055  bj-elsnb  37056  bj-snmoore  37108  bj-elsn0  37150  eldmressnALTV  38268  brressn  38439  zndvdchrrhm  41967  aks4d1p6  42076  aks6d1c2lem4  42122  sticksstones11  42151  aks6d1c6lem2  42166  aks6d1c7lem1  42175  rhmqusspan  42180  unitscyglem2  42191  reclimc  45658  itgsincmulx  45979  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem53  46164  fourierdlem58  46169  fourierdlem60  46171  fourierdlem61  46172  fourierdlem62  46173  fourierdlem76  46187  fourierdlem101  46212  elaa2  46239  etransc  46288  qndenserrnbl  46300  sge0tsms  46385  el1fzopredsuc  47330  elclnbgrelnbgr  47830  clnbupgrel  47839  mndtcob  49575