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

Theorem unisng 3845
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
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 sneq 3652 . . . 4  |-  ( x  =  A  ->  { x }  =  { A } )
21unieqd 3839 . . 3  |-  ( x  =  A  ->  U. {
x }  =  U. { A } )
3 id 19 . . 3  |-  ( x  =  A  ->  x  =  A )
42, 3eqeq12d 2298 . 2  |-  ( x  =  A  ->  ( U. { x }  =  x 
<-> 
U. { A }  =  A ) )
5 vex 2792 . . 3  |-  x  e. 
_V
65unisn 3844 . 2  |-  U. {
x }  =  x
74, 6vtoclg 2844 1  |-  ( A  e.  V  ->  U. { A }  =  A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1685   {csn 3641   U.cuni 3828
This theorem is referenced by:  dfnfc2  3846  unisn2  4521  unisn3  4522  dprdsn  15267  indistopon  16734  ordtuni  16916  cmpcld  17125  ptcmplem5  17746  cldsubg  17789  icccmplem2  18324  vmappw  20350  chsupsn  21988  cvmscld  23211  unisnif  23874  unexun  24980  topjoin  25725  fnejoin2  25729  heiborlem8  25953  en2other2  26793  pmtrprfv  26807
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-rex 2550  df-v 2791  df-un 3158  df-sn 3647  df-pr 3648  df-uni 3829
  Copyright terms: Public domain W3C validator