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

Theorem elsng 4138
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 2613 . 2 (𝑥 = 𝐴 → (𝑥 = 𝐵𝐴 = 𝐵))
2 df-sn 4125 . 2 {𝐵} = {𝑥𝑥 = 𝐵}
31, 2elab2g 3321 1 (𝐴𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1976  {csn 4124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-sn 4125
This theorem is referenced by:  elsn  4139  elsni  4141  snidg  4152  nelsnOLD  4159  eltpg  4173  eldifsn  4259  sneqrg  4305  elsucg  5695  ltxr  11784  elfzp12  12243  fprodn0f  14507  lcmfunsnlem2  15137  ramcl  15517  initoeu2lem1  16433  pmtrdifellem4  17668  logbmpt  24243  2lgslem2  24837  nbcusgra  25758  frgrancvvdeqlem1  26323  xrge0tsmsbi  28923  elzrhunit  29157  elzdif0  29158  esumrnmpt2  29263  plymulx  29757  bj-projval  31973  reclimc  38517  itgsincmulx  38663  dirkercncflem2  38794  dirkercncflem4  38796  fourierdlem53  38849  fourierdlem58  38854  fourierdlem60  38856  fourierdlem61  38857  fourierdlem62  38858  fourierdlem76  38872  fourierdlem101  38897  elaa2  38924  etransc  38973  qndenserrnbl  38988  sge0tsms  39070  el1fzopredsuc  39746  frgrncvvdeqlem1  41464
  Copyright terms: Public domain W3C validator