Theorem elsng 4605

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-sn 4592

This theorem is used by:  elsn  4606  elsni  4608  snidg  4628  elunsn  4651  eltpg  4654  el7g  4658  eldifsn  4755  sneqrg  4806  elsucg  6435  ltxr  13156  elfzp12  13648  fzdif1  13650  fprodn0f  16068  lcmfunsnlem2  16720  ramcl  17111  initoeu2lem1  18093  pmtrdifellem4  19593  psdmul  22379  plymulidp  26494  logbmpt  27004  2lgslem2  27610  xrge0tsmsbi  33458  rprmnz  33874  dimkerim  34081  elzrhunit  34431  esumrnmpt2  34522  bj-projval  37689  bj-elsn12g  37753  bj-elsnb  37754  bj-snmoore  37812  bj-elsn0  37856  eldmressnALTV  38986  brressn  39238  zndvdchrrhm  42798  aks4d1p6  42906  aks6d1c2lem4  42952  sticksstones11  42981  aks6d1c6lem2  42996  aks6d1c7lem1  43005  rhmqusspan  43010  unitscyglem2  43021  reclimc  46425  itgsincmulx  46746  dirkercncflem2  46876  dirkercncflem4  46878  fourierdlem53  46931  fourierdlem58  46936  fourierdlem60  46938  fourierdlem61  46939  fourierdlem62  46940  fourierdlem76  46954  fourierdlem101  46979  elaa2  47006  etransc  47055  qndenserrnbl  47067  sge0tsms  47152  el1fzopredsuc  48121  elclnbgrelnbgr  48648  clnbupgrel  48657  mndtcob  50417