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

Theorem elsng 4328
 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 2774 . 2 (𝑥 = 𝐴 → (𝑥 = 𝐵𝐴 = 𝐵))
2 df-sn 4315 . 2 {𝐵} = {𝑥𝑥 = 𝐵}
31, 2elab2g 3502 1 (𝐴𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1630   ∈ wcel 2144  {csn 4314 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-sn 4315 This theorem is referenced by:  elsn  4329  elsni  4331  snidg  4343  eltpg  4362  eldifsn  4451  sneqrg  4501  elsucg  5935  ltxr  12153  elfzp12  12625  fprodn0f  14927  lcmfunsnlem2  15560  ramcl  15939  initoeu2lem1  16870  pmtrdifellem4  18105  logbmpt  24746  2lgslem2  25340  xrge0tsmsbi  30120  elzrhunit  30357  elzdif0  30358  esumrnmpt2  30464  plymulx  30959  bj-projval  33309  bj-snmoore  33393  reclimc  40397  itgsincmulx  40701  dirkercncflem2  40832  dirkercncflem4  40834  fourierdlem53  40887  fourierdlem58  40892  fourierdlem60  40894  fourierdlem61  40895  fourierdlem62  40896  fourierdlem76  40910  fourierdlem101  40935  elaa2  40962  etransc  41011  qndenserrnbl  41026  sge0tsms  41108  el1fzopredsuc  41853
 Copyright terms: Public domain W3C validator