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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sn 4583

This theorem is referenced by:  elsn  4597  elsni  4599  snidg  4619  elunsn  4642  eltpg  4645  el7g  4649  eldifsn  4744  sneqrg  4797  elsucg  6395  ltxr  13041  elfzp12  13531  fzdif1  13533  fprodn0f  15926  lcmfunsnlem2  16579  ramcl  16969  initoeu2lem1  17950  pmtrdifellem4  19420  psdmul  22121  logbmpt  26766  2lgslem2  27374  xrge0tsmsbi  33168  rprmnz  33613  dimkerim  33805  elzrhunit  34155  esumrnmpt2  34246  plymulx  34726  bj-projval  37244  bj-elsn12g  37308  bj-elsnb  37309  bj-snmoore  37366  bj-elsn0  37410  eldmressnALTV  38530  brressn  38782  zndvdchrrhm  42342  aks4d1p6  42451  aks6d1c2lem4  42497  sticksstones11  42526  aks6d1c6lem2  42541  aks6d1c7lem1  42550  rhmqusspan  42555  unitscyglem2  42566  reclimc  46011  itgsincmulx  46332  dirkercncflem2  46462  dirkercncflem4  46464  fourierdlem53  46517  fourierdlem58  46522  fourierdlem60  46524  fourierdlem61  46525  fourierdlem62  46526  fourierdlem76  46540  fourierdlem101  46565  elaa2  46592  etransc  46641  qndenserrnbl  46653  sge0tsms  46738  el1fzopredsuc  47685  elclnbgrelnbgr  48185  clnbupgrel  48194  mndtcob  49941