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

Theorem unisng 4852
 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 4577 . . . 4 {𝐴} = {𝐴, 𝐴}
21unieqi 4846 . . 3 {𝐴} = {𝐴, 𝐴}
32a1i 11 . 2 (𝐴𝑉 {𝐴} = {𝐴, 𝐴})
4 uniprg 4851 . . 3 ((𝐴𝑉𝐴𝑉) → {𝐴, 𝐴} = (𝐴𝐴))
54anidms 567 . 2 (𝐴𝑉 {𝐴, 𝐴} = (𝐴𝐴))
6 unidm 4132 . . 3 (𝐴𝐴) = 𝐴
76a1i 11 . 2 (𝐴𝑉 → (𝐴𝐴) = 𝐴)
83, 5, 73eqtrd 2865 1 (𝐴𝑉 {𝐴} = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1530   ∈ wcel 2107   ∪ cun 3938  {csn 4564  {cpr 4566  ∪ cuni 4837 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rex 3149  df-v 3502  df-un 3945  df-sn 4565  df-pr 4567  df-uni 4838 This theorem is referenced by:  unisn  4853  unisn3  4854  dfnfc2  4855  unisn2  5213  en2other2  9429  pmtrprfv  18517  dprdsn  19094  indistopon  21544  ordtuni  21733  cmpcld  21945  ptcmplem5  22599  cldsubg  22653  icccmplem2  23365  vmappw  25626  chsupsn  29123  xrge0tsmseq  30627  cycpm2tr  30694  qustrivr  30863  esumsnf  31228  prsiga  31295  rossros  31344  cvmscld  32423  unisnif  33289  topjoin  33616  fnejoin2  33620  bj-snmoore  34305  pibt2  34586  heiborlem8  34983  fourierdlem80  42356
 Copyright terms: Public domain W3C validator