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

Theorem unisng 3844
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 3651 . . . 4  |-  ( x  =  A  ->  { x }  =  { A } )
21unieqd 3838 . . 3  |-  ( x  =  A  ->  U. {
x }  =  U. { A } )
3 id 19 . . 3  |-  ( x  =  A  ->  x  =  A )
42, 3eqeq12d 2297 . 2  |-  ( x  =  A  ->  ( U. { x }  =  x 
<-> 
U. { A }  =  A ) )
5 vex 2791 . . 3  |-  x  e. 
_V
65unisn 3843 . 2  |-  U. {
x }  =  x
74, 6vtoclg 2843 1  |-  ( A  e.  V  ->  U. { A }  =  A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   {csn 3640   U.cuni 3827
This theorem is referenced by:  dfnfc2  3845  unisn2  4522  unisn3  4523  dprdsn  15271  indistopon  16738  ordtuni  16920  cmpcld  17129  ptcmplem5  17750  cldsubg  17793  icccmplem2  18328  vmappw  20354  chsupsn  21992  xrge0tsmseq  23384  esumsn  23437  prsiga  23492  cvmscld  23804  unisnif  24464  unexun  25569  topjoin  26314  fnejoin2  26318  heiborlem8  26542  en2other2  27382  pmtrprfv  27396
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 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
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 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-v 2790  df-un 3157  df-sn 3646  df-pr 3647  df-uni 3828
  Copyright terms: Public domain W3C validator