Theorem elsng 4596

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560   ∈ wcel 2142  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-sn 4583

This theorem is referenced by:  elsn  4597  elsni  4599  snidg  4619  elunsn  4642  eltpg  4645  el7g  4649  eldifsn  4746  sneqrg  4797  elsucg  6416  ltxr  13117  elfzp12  13608  fzdif1  13610  fprodn0f  16021  lcmfunsnlem2  16674  ramcl  17065  initoeu2lem1  18047  pmtrdifellem4  19519  psdmul  22228  plymulidp  26343  logbmpt  26850  2lgslem2  27456  xrge0tsmsbi  33251  rprmnz  33713  dimkerim  33921  elzrhunit  34271  esumrnmpt2  34362  bj-projval  37478  bj-elsn12g  37542  bj-elsnb  37543  bj-snmoore  37600  bj-elsn0  37644  eldmressnALTV  38775  brressn  39027  zndvdchrrhm  42587  aks4d1p6  42695  aks6d1c2lem4  42741  sticksstones11  42770  aks6d1c6lem2  42785  aks6d1c7lem1  42794  rhmqusspan  42799  unitscyglem2  42810  reclimc  46224  itgsincmulx  46545  dirkercncflem2  46675  dirkercncflem4  46677  fourierdlem53  46730  fourierdlem58  46735  fourierdlem60  46737  fourierdlem61  46738  fourierdlem62  46739  fourierdlem76  46753  fourierdlem101  46778  elaa2  46805  etransc  46854  qndenserrnbl  46866  sge0tsms  46951  el1fzopredsuc  47917  elclnbgrelnbgr  48444  clnbupgrel  48453  mndtcob  50200