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

Theorem elsng 4571
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.
StepHypRef Expression
1 eqeq1 2822 . 2 (𝑥 = 𝐴 → (𝑥 = 𝐵𝐴 = 𝐵))
2 df-sn 4558 . 2 {𝐵} = {𝑥𝑥 = 𝐵}
31, 2elab2g 3665 1 (𝐴𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105  {csn 4557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-sn 4558
This theorem is referenced by:  elsn  4572  elsni  4574  snidg  4589  eltpg  4615  eldifsn  4711  eldifsnneqOLD  4716  sneqrg  4762  elsucg  6251  ltxr  12498  elfzp12  12974  fprodn0f  15333  lcmfunsnlem2  15972  ramcl  16353  initoeu2lem1  17262  pmtrdifellem4  18536  logbmpt  25293  2lgslem2  25898  elunsn  30200  xrge0tsmsbi  30620  dimkerim  30922  elzrhunit  31119  esumrnmpt2  31226  plymulx  31717  bj-projval  34205  bj-elsn12g  34247  bj-elsnb  34248  bj-snmoore  34299  bj-elsn0  34339  reclimc  41810  itgsincmulx  42135  dirkercncflem2  42266  dirkercncflem4  42268  fourierdlem53  42321  fourierdlem58  42326  fourierdlem60  42328  fourierdlem61  42329  fourierdlem62  42330  fourierdlem76  42344  fourierdlem101  42369  elaa2  42396  etransc  42445  qndenserrnbl  42457  sge0tsms  42539  el1fzopredsuc  43402
  Copyright terms: Public domain W3C validator