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  17956  pmtrdifellem4  19393  psdmul  22086  logbmpt  26731  2lgslem2  27339  xrge0tsmsbi  33046  rprmnz  33484  dimkerim  33616  elzrhunit  33960  esumrnmpt2  34051  plymulx  34532  bj-projval  36977  bj-elsn12g  37041  bj-elsnb  37042  bj-snmoore  37094  bj-elsn0  37136  eldmressnALTV  38254  brressn  38425  zndvdchrrhm  41953  aks4d1p6  42062  aks6d1c2lem4  42108  sticksstones11  42137  aks6d1c6lem2  42152  aks6d1c7lem1  42161  rhmqusspan  42166  unitscyglem2  42177  reclimc  45644  itgsincmulx  45965  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem53  46150  fourierdlem58  46155  fourierdlem60  46157  fourierdlem61  46158  fourierdlem62  46159  fourierdlem76  46173  fourierdlem101  46198  elaa2  46225  etransc  46274  qndenserrnbl  46286  sge0tsms  46371  el1fzopredsuc  47319  elclnbgrelnbgr  47819  clnbupgrel  47828  mndtcob  49564