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

Theorem unisng 3946
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 3740 . . . 4  |-  ( x  =  A  ->  { x }  =  { A } )
21unieqd 3940 . . 3  |-  ( x  =  A  ->  U. {
x }  =  U. { A } )
3 id 19 . . 3  |-  ( x  =  A  ->  x  =  A )
42, 3eqeq12d 2380 . 2  |-  ( x  =  A  ->  ( U. { x }  =  x 
<-> 
U. { A }  =  A ) )
5 vex 2876 . . 3  |-  x  e. 
_V
65unisn 3945 . 2  |-  U. {
x }  =  x
74, 6vtoclg 2928 1  |-  ( A  e.  V  ->  U. { A }  =  A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1647    e. wcel 1715   {csn 3729   U.cuni 3929
This theorem is referenced by:  dfnfc2  3947  unisn2  4625  unisn3  4626  dprdsn  15481  indistopon  16955  ordtuni  17137  cmpcld  17346  ptcmplem5  17963  cldsubg  18006  icccmplem2  18542  vmappw  20577  chsupsn  22426  xrge0tsmseq  23737  esumsn  24042  prsiga  24100  cvmscld  24528  unisnif  25290  topjoin  25906  fnejoin2  25910  heiborlem8  26133  en2other2  26973  pmtrprfv  26987
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rex 2634  df-v 2875  df-un 3243  df-sn 3735  df-pr 3736  df-uni 3930
  Copyright terms: Public domain W3C validator