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

Theorem elsng 4182
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 2624 . 2 (𝑥 = 𝐴 → (𝑥 = 𝐵𝐴 = 𝐵))
2 df-sn 4169 . 2 {𝐵} = {𝑥𝑥 = 𝐵}
31, 2elab2g 3347 1 (𝐴𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  wcel 1988  {csn 4168
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-sn 4169
This theorem is referenced by:  elsn  4183  elsni  4185  snidg  4197  nelsnOLD  4204  eltpg  4218  eldifsn  4308  sneqrg  4361  elsucg  5780  ltxr  11934  elfzp12  12403  fprodn0f  14703  lcmfunsnlem2  15334  ramcl  15714  initoeu2lem1  16645  pmtrdifellem4  17880  logbmpt  24507  2lgslem2  25101  xrge0tsmsbi  29760  elzrhunit  29997  elzdif0  29998  esumrnmpt2  30104  plymulx  30599  bj-projval  32959  bj-snmoore  33043  reclimc  39685  itgsincmulx  39953  dirkercncflem2  40084  dirkercncflem4  40086  fourierdlem53  40139  fourierdlem58  40144  fourierdlem60  40146  fourierdlem61  40147  fourierdlem62  40148  fourierdlem76  40162  fourierdlem101  40187  elaa2  40214  etransc  40263  qndenserrnbl  40278  sge0tsms  40360  el1fzopredsuc  41098
  Copyright terms: Public domain W3C validator