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

Theorem unisng 3744
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  |-  ( A  e.  V  ->  U. { A }  =  A
)

Proof of Theorem unisng
StepHypRef Expression
1 sneq 3555 . . . 4  |-  ( x  =  A  ->  { x }  =  { A } )
21unieqd 3738 . . 3  |-  ( x  =  A  ->  U. {
x }  =  U. { A } )
3 id 21 . . 3  |-  ( x  =  A  ->  x  =  A )
42, 3eqeq12d 2267 . 2  |-  ( x  =  A  ->  ( U. { x }  =  x 
<-> 
U. { A }  =  A ) )
5 vex 2730 . . 3  |-  x  e. 
_V
65unisn 3743 . 2  |-  U. {
x }  =  x
74, 6vtoclg 2781 1  |-  ( A  e.  V  ->  U. { A }  =  A
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    e. wcel 1621   {csn 3544   U.cuni 3727
This theorem is referenced by:  dfnfc2  3745  unisn2  4413  unisn3  4414  dprdsn  15106  indistopon  16570  ordtuni  16752  cmpcld  16961  ptcmplem5  17582  cldsubg  17625  icccmplem2  18160  vmappw  20186  chsupsn  21822  cvmscld  22975  unisnif  23638  unexun  24735  topjoin  25480  fnejoin2  25484  heiborlem8  25708  en2other2  26548  pmtrprfv  26562
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-rex 2514  df-v 2729  df-un 3083  df-sn 3550  df-pr 3551  df-uni 3728
  Copyright terms: Public domain W3C validator