Theorem elsng 4647

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099  {csn 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-sn 4634

This theorem is referenced by:  elsn  4648  elsni  4650  snidg  4667  eltpg  4694  eldifsn  4795  sneqrg  4846  elsucg  6444  ltxr  13149  elfzp12  13634  fprodn0f  15993  lcmfunsnlem2  16641  ramcl  17031  initoeu2lem1  18036  pmtrdifellem4  19477  psdmul  22160  logbmpt  26816  2lgslem2  27424  elunsn  32438  xrge0tsmsbi  32927  rprmnz  33395  dimkerim  33522  elzrhunit  33794  esumrnmpt2  33901  plymulx  34394  bj-projval  36703  bj-elsn12g  36767  bj-elsnb  36768  bj-snmoore  36820  bj-elsn0  36862  eldmressnALTV  37970  brressn  38139  zndvdchrrhm  41669  aks4d1p6  41780  aks6d1c2lem4  41825  sticksstones11  41854  aks6d1c6lem2  41869  aks6d1c7lem1  41878  rhmqusspan  41883  metakunt20  41910  reclimc  45274  itgsincmulx  45595  dirkercncflem2  45725  dirkercncflem4  45727  fourierdlem53  45780  fourierdlem58  45785  fourierdlem60  45787  fourierdlem61  45788  fourierdlem62  45789  fourierdlem76  45803  fourierdlem101  45828  elaa2  45855  etransc  45904  qndenserrnbl  45916  sge0tsms  46001  el1fzopredsuc  46938  clnbupgrel  47405  mndtcob  48409