Theorem elsng 4603

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-sn 4590

This theorem is referenced by:  elsn  4604  elsni  4606  snidg  4626  elunsn  4649  eltpg  4652  el7g  4656  eldifsn  4753  sneqrg  4804  elsucg  6431  ltxr  13135  elfzp12  13627  fzdif1  13629  fprodn0f  16041  lcmfunsnlem2  16693  ramcl  17084  initoeu2lem1  18066  pmtrdifellem4  19544  psdmul  22329  plymulidp  26443  logbmpt  26953  2lgslem2  27559  xrge0tsmsbi  33394  rprmnz  33810  dimkerim  34017  elzrhunit  34367  esumrnmpt2  34458  bj-projval  37632  bj-elsn12g  37696  bj-elsnb  37697  bj-snmoore  37755  bj-elsn0  37799  eldmressnALTV  38928  brressn  39180  zndvdchrrhm  42740  aks4d1p6  42848  aks6d1c2lem4  42894  sticksstones11  42923  aks6d1c6lem2  42938  aks6d1c7lem1  42947  rhmqusspan  42952  unitscyglem2  42963  reclimc  46367  itgsincmulx  46688  dirkercncflem2  46818  dirkercncflem4  46820  fourierdlem53  46873  fourierdlem58  46878  fourierdlem60  46880  fourierdlem61  46881  fourierdlem62  46882  fourierdlem76  46896  fourierdlem101  46921  elaa2  46948  etransc  46997  qndenserrnbl  47009  sge0tsms  47094  el1fzopredsuc  48063  elclnbgrelnbgr  48590  clnbupgrel  48599  mndtcob  50360