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

Theorem unisng 3846
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 3653 . . . 4  |-  ( x  =  A  ->  { x }  =  { A } )
21unieqd 3840 . . 3  |-  ( x  =  A  ->  U. {
x }  =  U. { A } )
3 id 19 . . 3  |-  ( x  =  A  ->  x  =  A )
42, 3eqeq12d 2299 . 2  |-  ( x  =  A  ->  ( U. { x }  =  x 
<-> 
U. { A }  =  A ) )
5 vex 2793 . . 3  |-  x  e. 
_V
65unisn 3845 . 2  |-  U. {
x }  =  x
74, 6vtoclg 2845 1  |-  ( A  e.  V  ->  U. { A }  =  A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625    e. wcel 1686   {csn 3642   U.cuni 3829
This theorem is referenced by:  dfnfc2  3847  unisn2  4524  unisn3  4525  dprdsn  15273  indistopon  16740  ordtuni  16922  cmpcld  17131  ptcmplem5  17752  cldsubg  17795  icccmplem2  18330  vmappw  20356  chsupsn  21994  xrge0tsmseq  23386  esumsn  23439  prsiga  23494  cvmscld  23806  unisnif  24466  unexun  25580  topjoin  26325  fnejoin2  26329  heiborlem8  26553  en2other2  27393  pmtrprfv  27407
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rex 2551  df-v 2792  df-un 3159  df-sn 3648  df-pr 3649  df-uni 3830
  Copyright terms: Public domain W3C validator