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

Theorem iunid 4114
Description: An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.)
Assertion
Ref Expression
iunid  |-  U_ x  e.  A  { x }  =  A
Distinct variable group:    x, A

Proof of Theorem iunid
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-sn 3788 . . . . 5  |-  { x }  =  { y  |  y  =  x }
2 equcom 1688 . . . . . 6  |-  ( y  =  x  <->  x  =  y )
32abbii 2524 . . . . 5  |-  { y  |  y  =  x }  =  { y  |  x  =  y }
41, 3eqtri 2432 . . . 4  |-  { x }  =  { y  |  x  =  y }
54a1i 11 . . 3  |-  ( x  e.  A  ->  { x }  =  { y  |  x  =  y } )
65iuneq2i 4079 . 2  |-  U_ x  e.  A  { x }  =  U_ x  e.  A  { y  |  x  =  y }
7 iunab 4105 . . 3  |-  U_ x  e.  A  { y  |  x  =  y }  =  { y  |  E. x  e.  A  x  =  y }
8 risset 2721 . . . 4  |-  ( y  e.  A  <->  E. x  e.  A  x  =  y )
98abbii 2524 . . 3  |-  { y  |  y  e.  A }  =  { y  |  E. x  e.  A  x  =  y }
10 abid2 2529 . . 3  |-  { y  |  y  e.  A }  =  A
117, 9, 103eqtr2i 2438 . 2  |-  U_ x  e.  A  { y  |  x  =  y }  =  A
126, 11eqtri 2432 1  |-  U_ x  e.  A  { x }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1721   {cab 2398   E.wrex 2675   {csn 3782   U_ciun 4061
This theorem is referenced by:  iunxpconst  4901  xpexgALT  6264  uniqs  6931  rankcf  8616  dprd2da  15563  t1ficld  17353  discmp  17423  xkoinjcn  17680  metnrmlem2  18851  ovoliunlem1  19359  i1fima  19531  i1fd  19534  itg1addlem5  19553  sibfof  24615  cvmlift2lem12  24962  dftrpred4g  25459  itg2addnclem2  26164  bnj1415  29125
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-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-ral 2679  df-rex 2680  df-v 2926  df-in 3295  df-ss 3302  df-sn 3788  df-iun 4063
  Copyright terms: Public domain W3C validator