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

Theorem elsng 4647
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 2730 . 2 (𝑥 = 𝐴 → (𝑥 = 𝐵𝐴 = 𝐵))
2 df-sn 4634 . 2 {𝐵} = {𝑥𝑥 = 𝐵}
31, 2elab2g 3668 1 (𝐴𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1534  wcel 2099  {csn 4633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-sn 4634
This theorem is referenced by:  elsn  4648  elsni  4650  snidg  4667  eltpg  4694  eldifsn  4795  sneqrg  4846  elsucg  6444  ltxr  13149  elfzp12  13634  fprodn0f  15993  lcmfunsnlem2  16641  ramcl  17031  initoeu2lem1  18036  pmtrdifellem4  19477  psdmul  22160  logbmpt  26816  2lgslem2  27424  elunsn  32438  xrge0tsmsbi  32927  rprmnz  33395  dimkerim  33522  elzrhunit  33794  esumrnmpt2  33901  plymulx  34394  bj-projval  36703  bj-elsn12g  36767  bj-elsnb  36768  bj-snmoore  36820  bj-elsn0  36862  eldmressnALTV  37970  brressn  38139  zndvdchrrhm  41669  aks4d1p6  41780  aks6d1c2lem4  41825  sticksstones11  41854  aks6d1c6lem2  41869  aks6d1c7lem1  41878  rhmqusspan  41883  metakunt20  41910  reclimc  45274  itgsincmulx  45595  dirkercncflem2  45725  dirkercncflem4  45727  fourierdlem53  45780  fourierdlem58  45785  fourierdlem60  45787  fourierdlem61  45788  fourierdlem62  45789  fourierdlem76  45803  fourierdlem101  45828  elaa2  45855  etransc  45904  qndenserrnbl  45916  sge0tsms  46001  el1fzopredsuc  46938  clnbupgrel  47405  mndtcob  48409
  Copyright terms: Public domain W3C validator