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

Theorem unisng 4128
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 3908 . . . 4  |-  ( x  =  A  ->  { x }  =  { A } )
21unieqd 4122 . . 3  |-  ( x  =  A  ->  U. {
x }  =  U. { A } )
3 id 22 . . 3  |-  ( x  =  A  ->  x  =  A )
42, 3eqeq12d 2457 . 2  |-  ( x  =  A  ->  ( U. { x }  =  x 
<-> 
U. { A }  =  A ) )
5 vex 2996 . . 3  |-  x  e. 
_V
65unisn 4127 . 2  |-  U. {
x }  =  x
74, 6vtoclg 3051 1  |-  ( A  e.  V  ->  U. { A }  =  A
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   {csn 3898   U.cuni 4112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rex 2742  df-v 2995  df-un 3354  df-sn 3899  df-pr 3901  df-uni 4113
This theorem is referenced by:  unisn3  4129  dfnfc2  4130  unisn2  4449  en2other2  8197  pmtrprfv  15980  dprdsn  16555  indistopon  18627  ordtuni  18816  cmpcld  19027  ptcmplem5  19650  cldsubg  19703  icccmplem2  20422  vmappw  22476  chsupsn  24838  xrge0tsmseq  26277  esumsn  26537  prsiga  26596  cvmscld  27184  unisnif  27978  topjoin  28612  fnejoin2  28616  heiborlem8  28743
  Copyright terms: Public domain W3C validator