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

Theorem unisng 4267
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 4043 . . . 4  |-  ( x  =  A  ->  { x }  =  { A } )
21unieqd 4261 . . 3  |-  ( x  =  A  ->  U. {
x }  =  U. { A } )
3 id 22 . . 3  |-  ( x  =  A  ->  x  =  A )
42, 3eqeq12d 2489 . 2  |-  ( x  =  A  ->  ( U. { x }  =  x 
<-> 
U. { A }  =  A ) )
5 vex 3121 . . 3  |-  x  e. 
_V
65unisn 4266 . 2  |-  U. {
x }  =  x
74, 6vtoclg 3176 1  |-  ( A  e.  V  ->  U. { A }  =  A
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767   {csn 4033   U.cuni 4251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2823  df-v 3120  df-un 3486  df-sn 4034  df-pr 4036  df-uni 4252
This theorem is referenced by:  unisn3  4268  dfnfc2  4269  unisn2  4589  en2other2  8399  pmtrprfv  16351  dprdsn  16955  indistopon  19370  ordtuni  19559  cmpcld  19770  ptcmplem5  20424  cldsubg  20477  icccmplem2  21196  vmappw  23256  chsupsn  26154  xrge0tsmseq  27602  esumsn  27897  prsiga  27956  cvmscld  28543  unisnif  29502  topjoin  30110  fnejoin2  30114  heiborlem8  30241  fourierdlem80  31810
  Copyright terms: Public domain W3C validator