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

Theorem unisng 4845
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 4570 . . . 4 {𝐴} = {𝐴, 𝐴}
21unieqi 4839 . . 3 {𝐴} = {𝐴, 𝐴}
32a1i 11 . 2 (𝐴𝑉 {𝐴} = {𝐴, 𝐴})
4 uniprg 4844 . . 3 ((𝐴𝑉𝐴𝑉) → {𝐴, 𝐴} = (𝐴𝐴))
54anidms 567 . 2 (𝐴𝑉 {𝐴, 𝐴} = (𝐴𝐴))
6 unidm 4125 . . 3 (𝐴𝐴) = 𝐴
76a1i 11 . 2 (𝐴𝑉 → (𝐴𝐴) = 𝐴)
83, 5, 73eqtrd 2857 1 (𝐴𝑉 {𝐴} = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  cun 3931  {csn 4557  {cpr 4559   cuni 4830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-v 3494  df-un 3938  df-sn 4558  df-pr 4560  df-uni 4831
This theorem is referenced by:  unisn  4846  unisn3  4847  dfnfc2  4848  unisn2  5207  en2other2  9423  pmtrprfv  18510  dprdsn  19087  indistopon  21537  ordtuni  21726  cmpcld  21938  ptcmplem5  22592  cldsubg  22646  icccmplem2  23358  vmappw  25620  chsupsn  29117  xrge0tsmseq  30621  cycpm2tr  30688  qustrivr  30857  esumsnf  31222  prsiga  31289  rossros  31338  cvmscld  32417  unisnif  33283  topjoin  33610  fnejoin2  33614  bj-snmoore  34299  pibt2  34580  heiborlem8  34977  fourierdlem80  42348
  Copyright terms: Public domain W3C validator