MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elsng Structured version   Visualization version   GIF version

Theorem elsng 4539
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 variables 𝑦 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqeq1 2802 . 2 (𝑥 = 𝑦 → (𝑥 = 𝐵𝑦 = 𝐵))
2 eqeq1 2802 . 2 (𝑦 = 𝐴 → (𝑦 = 𝐵𝐴 = 𝐵))
3 df-sn 4526 . 2 {𝐵} = {𝑥𝑥 = 𝐵}
41, 2, 3elab2gw 3613 1 (𝐴𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wcel 2111  {csn 4525
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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-sn 4526
This theorem is referenced by:  elsn  4540  elsni  4542  snidg  4559  eltpg  4583  eldifsn  4680  sneqrg  4730  elsucg  6226  ltxr  12498  elfzp12  12981  fprodn0f  15337  lcmfunsnlem2  15974  ramcl  16355  initoeu2lem1  17266  pmtrdifellem4  18599  logbmpt  25374  2lgslem2  25979  elunsn  30281  xrge0tsmsbi  30743  dimkerim  31111  elzrhunit  31330  esumrnmpt2  31437  plymulx  31928  bj-projval  34432  bj-elsn12g  34477  bj-elsnb  34478  bj-snmoore  34528  bj-elsn0  34570  metakunt20  39367  reclimc  42293  itgsincmulx  42614  dirkercncflem2  42744  dirkercncflem4  42746  fourierdlem53  42799  fourierdlem58  42804  fourierdlem60  42806  fourierdlem61  42807  fourierdlem62  42808  fourierdlem76  42822  fourierdlem101  42847  elaa2  42874  etransc  42923  qndenserrnbl  42935  sge0tsms  43017  el1fzopredsuc  43880
  Copyright terms: Public domain W3C validator