Theorem elsng 4575

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-sn 4562

This theorem is referenced by:  elsn  4576  elsni  4578  snidg  4595  eltpg  4621  eldifsn  4720  sneqrg  4770  elsucg  6333  ltxr  12851  elfzp12  13335  fprodn0f  15701  lcmfunsnlem2  16345  ramcl  16730  initoeu2lem1  17729  pmtrdifellem4  19087  logbmpt  25938  2lgslem2  26543  elunsn  30858  xrge0tsmsbi  31318  dimkerim  31708  elzrhunit  31929  esumrnmpt2  32036  plymulx  32527  bj-projval  35186  bj-elsn12g  35231  bj-elsnb  35232  bj-snmoore  35284  bj-elsn0  35326  aks4d1p6  40089  sticksstones11  40112  metakunt20  40144  reclimc  43194  itgsincmulx  43515  dirkercncflem2  43645  dirkercncflem4  43647  fourierdlem53  43700  fourierdlem58  43705  fourierdlem60  43707  fourierdlem61  43708  fourierdlem62  43709  fourierdlem76  43723  fourierdlem101  43748  elaa2  43775  etransc  43824  qndenserrnbl  43836  sge0tsms  43918  el1fzopredsuc  44817  mndtcob  46369