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

Theorem unisng 4860
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 4574 . . . 4 {𝐴} = {𝐴, 𝐴}
21unieqi 4852 . . 3 {𝐴} = {𝐴, 𝐴}
32a1i 11 . 2 (𝐴𝑉 {𝐴} = {𝐴, 𝐴})
4 uniprg 4856 . . 3 ((𝐴𝑉𝐴𝑉) → {𝐴, 𝐴} = (𝐴𝐴))
54anidms 567 . 2 (𝐴𝑉 {𝐴, 𝐴} = (𝐴𝐴))
6 unidm 4086 . . 3 (𝐴𝐴) = 𝐴
76a1i 11 . 2 (𝐴𝑉 → (𝐴𝐴) = 𝐴)
83, 5, 73eqtrd 2782 1 (𝐴𝑉 {𝐴} = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wcel 2106  cun 3885  {csn 4561  {cpr 4563   cuni 4839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-sn 4562  df-pr 4564  df-uni 4840
This theorem is referenced by:  unisn  4861  unisn3  4862  dfnfc2  4863  unisn2  5236  en2other2  9765  pmtrprfv  19061  dprdsn  19639  indistopon  22151  ordtuni  22341  cmpcld  22553  ptcmplem5  23207  cldsubg  23262  icccmplem2  23986  vmappw  26265  chsupsn  29775  xrge0tsmseq  31319  cycpm2tr  31386  qustrivr  31561  esumsnf  32032  prsiga  32099  rossros  32148  cvmscld  33235  unisnif  34227  topjoin  34554  fnejoin2  34558  bj-snmoore  35284  pibt2  35588  heiborlem8  35976  nlimsuc  41048  fourierdlem80  43727
  Copyright terms: Public domain W3C validator