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

Theorem unisng 4641
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 4380 . . . 4 {𝐴} = {𝐴, 𝐴}
21unieqi 4635 . . 3 {𝐴} = {𝐴, 𝐴}
32a1i 11 . 2 (𝐴𝑉 {𝐴} = {𝐴, 𝐴})
4 uniprg 4640 . . 3 ((𝐴𝑉𝐴𝑉) → {𝐴, 𝐴} = (𝐴𝐴))
54anidms 558 . 2 (𝐴𝑉 {𝐴, 𝐴} = (𝐴𝐴))
6 unidm 3952 . . 3 (𝐴𝐴) = 𝐴
76a1i 11 . 2 (𝐴𝑉 → (𝐴𝐴) = 𝐴)
83, 5, 73eqtrd 2843 1 (𝐴𝑉 {𝐴} = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2158  cun 3764  {csn 4367  {cpr 4369   cuni 4626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-rex 3101  df-v 3392  df-un 3771  df-sn 4368  df-pr 4370  df-uni 4627
This theorem is referenced by:  unisn  4642  unisn3  4645  dfnfc2  4646  unisn2  4986  en2other2  9112  pmtrprfv  18070  dprdsn  18633  indistopon  21015  ordtuni  21204  cmpcld  21415  ptcmplem5  22069  cldsubg  22123  icccmplem2  22835  vmappw  25052  chsupsn  28597  xrge0tsmseq  30109  esumsnf  30448  prsiga  30516  rossros  30565  cvmscld  31575  unisnif  32350  topjoin  32678  fnejoin2  32682  bj-snmoore  33376  heiborlem8  33925  fourierdlem80  40879
  Copyright terms: Public domain W3C validator