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

Theorem unisng 3923
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 3727 . . . 4  |-  ( x  =  A  ->  { x }  =  { A } )
21unieqd 3917 . . 3  |-  ( x  =  A  ->  U. {
x }  =  U. { A } )
3 id 19 . . 3  |-  ( x  =  A  ->  x  =  A )
42, 3eqeq12d 2372 . 2  |-  ( x  =  A  ->  ( U. { x }  =  x 
<-> 
U. { A }  =  A ) )
5 vex 2867 . . 3  |-  x  e. 
_V
65unisn 3922 . 2  |-  U. {
x }  =  x
74, 6vtoclg 2919 1  |-  ( A  e.  V  ->  U. { A }  =  A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642    e. wcel 1710   {csn 3716   U.cuni 3906
This theorem is referenced by:  dfnfc2  3924  unisn2  4601  unisn3  4602  dprdsn  15364  indistopon  16838  ordtuni  17020  cmpcld  17229  ptcmplem5  17846  cldsubg  17889  icccmplem2  18425  vmappw  20460  chsupsn  22100  xrge0tsmseq  23417  esumsn  23722  prsiga  23780  cvmscld  24208  unisnif  25022  topjoin  25638  fnejoin2  25642  heiborlem8  25865  en2other2  26705  pmtrprfv  26719
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rex 2625  df-v 2866  df-un 3233  df-sn 3722  df-pr 3723  df-uni 3907
  Copyright terms: Public domain W3C validator