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

Theorem unisng 4000
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 3793 . . . 4  |-  ( x  =  A  ->  { x }  =  { A } )
21unieqd 3994 . . 3  |-  ( x  =  A  ->  U. {
x }  =  U. { A } )
3 id 20 . . 3  |-  ( x  =  A  ->  x  =  A )
42, 3eqeq12d 2426 . 2  |-  ( x  =  A  ->  ( U. { x }  =  x 
<-> 
U. { A }  =  A ) )
5 vex 2927 . . 3  |-  x  e. 
_V
65unisn 3999 . 2  |-  U. {
x }  =  x
74, 6vtoclg 2979 1  |-  ( A  e.  V  ->  U. { A }  =  A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721   {csn 3782   U.cuni 3983
This theorem is referenced by:  dfnfc2  4001  unisn2  4678  unisn3  4679  dprdsn  15557  indistopon  17028  ordtuni  17216  cmpcld  17427  ptcmplem5  18048  cldsubg  18101  icccmplem2  18815  vmappw  20860  chsupsn  22876  xrge0tsmseq  24186  esumsn  24417  prsiga  24475  cvmscld  24921  unisnif  25686  topjoin  26292  fnejoin2  26296  heiborlem8  26425  en2other2  27258  pmtrprfv  27272
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rex 2680  df-v 2926  df-un 3293  df-sn 3788  df-pr 3789  df-uni 3984
  Copyright terms: Public domain W3C validator