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

Theorem unisng 4827
Description: A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 13-Aug-2002.)
Assertion
Ref Expression
unisng (𝐴𝑉 {𝐴} = 𝐴)

Proof of Theorem unisng
StepHypRef Expression
1 dfsn2 4539 . . . 4 {𝐴} = {𝐴, 𝐴}
21unieqi 4819 . . 3 {𝐴} = {𝐴, 𝐴}
32a1i 11 . 2 (𝐴𝑉 {𝐴} = {𝐴, 𝐴})
4 uniprg 4823 . . 3 ((𝐴𝑉𝐴𝑉) → {𝐴, 𝐴} = (𝐴𝐴))
54anidms 570 . 2 (𝐴𝑉 {𝐴, 𝐴} = (𝐴𝐴))
6 unidm 4052 . . 3 (𝐴𝐴) = 𝐴
76a1i 11 . 2 (𝐴𝑉 → (𝐴𝐴) = 𝐴)
83, 5, 73eqtrd 2778 1 (𝐴𝑉 {𝐴} = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2114  cun 3851  {csn 4526  {cpr 4528   cuni 4806
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-un 3858  df-in 3860  df-ss 3870  df-sn 4527  df-pr 4529  df-uni 4807
This theorem is referenced by:  unisn  4828  unisn3  4829  dfnfc2  4830  unisn2  5190  en2other2  9522  pmtrprfv  18712  dprdsn  19290  indistopon  21765  ordtuni  21954  cmpcld  22166  ptcmplem5  22820  cldsubg  22875  icccmplem2  23588  vmappw  25866  chsupsn  29361  xrge0tsmseq  30909  cycpm2tr  30976  qustrivr  31146  esumsnf  31615  prsiga  31682  rossros  31731  cvmscld  32819  unisnif  33883  topjoin  34210  fnejoin2  34214  bj-snmoore  34938  pibt2  35244  heiborlem8  35632  fourierdlem80  43310
  Copyright terms: Public domain W3C validator