Theorem elsng 4599

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sn 4586

This theorem is referenced by:  elsn  4600  elsni  4602  snidg  4620  elunsn  4643  eltpg  4646  el7g  4650  eldifsn  4746  sneqrg  4799  elsucg  6390  ltxr  13051  elfzp12  13540  fzdif1  13542  fprodn0f  15933  lcmfunsnlem2  16586  ramcl  16976  initoeu2lem1  17952  pmtrdifellem4  19385  psdmul  22029  logbmpt  26674  2lgslem2  27282  xrge0tsmsbi  32976  rprmnz  33464  dimkerim  33596  elzrhunit  33940  esumrnmpt2  34031  plymulx  34512  bj-projval  36957  bj-elsn12g  37021  bj-elsnb  37022  bj-snmoore  37074  bj-elsn0  37116  eldmressnALTV  38234  brressn  38405  zndvdchrrhm  41933  aks4d1p6  42042  aks6d1c2lem4  42088  sticksstones11  42117  aks6d1c6lem2  42132  aks6d1c7lem1  42141  rhmqusspan  42146  unitscyglem2  42157  reclimc  45624  itgsincmulx  45945  dirkercncflem2  46075  dirkercncflem4  46077  fourierdlem53  46130  fourierdlem58  46135  fourierdlem60  46137  fourierdlem61  46138  fourierdlem62  46139  fourierdlem76  46153  fourierdlem101  46178  elaa2  46205  etransc  46254  qndenserrnbl  46266  sge0tsms  46351  el1fzopredsuc  47299  elclnbgrelnbgr  47799  clnbupgrel  47808  mndtcob  49544