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

Theorem iunid 4148
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 3822 . . . . 5  |-  { x }  =  { y  |  y  =  x }
2 equcom 1693 . . . . . 6  |-  ( y  =  x  <->  x  =  y )
32abbii 2550 . . . . 5  |-  { y  |  y  =  x }  =  { y  |  x  =  y }
41, 3eqtri 2458 . . . 4  |-  { x }  =  { y  |  x  =  y }
54a1i 11 . . 3  |-  ( x  e.  A  ->  { x }  =  { y  |  x  =  y } )
65iuneq2i 4113 . 2  |-  U_ x  e.  A  { x }  =  U_ x  e.  A  { y  |  x  =  y }
7 iunab 4139 . . 3  |-  U_ x  e.  A  { y  |  x  =  y }  =  { y  |  E. x  e.  A  x  =  y }
8 risset 2755 . . . 4  |-  ( y  e.  A  <->  E. x  e.  A  x  =  y )
98abbii 2550 . . 3  |-  { y  |  y  e.  A }  =  { y  |  E. x  e.  A  x  =  y }
10 abid2 2555 . . 3  |-  { y  |  y  e.  A }  =  A
117, 9, 103eqtr2i 2464 . 2  |-  U_ x  e.  A  { y  |  x  =  y }  =  A
126, 11eqtri 2458 1  |-  U_ x  e.  A  { x }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1653    e. wcel 1726   {cab 2424   E.wrex 2708   {csn 3816   U_ciun 4095
This theorem is referenced by:  iunxpconst  4937  xpexgALT  6300  uniqs  6967  rankcf  8657  dprd2da  15605  t1ficld  17396  discmp  17466  xkoinjcn  17724  metnrmlem2  18895  ovoliunlem1  19403  i1fima  19573  i1fd  19576  itg1addlem5  19595  sibfof  24659  cvmlift2lem12  25006  dftrpred4g  25517  itg2addnclem2  26271  ftc1anclem6  26299  bnj1415  29481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-v 2960  df-in 3329  df-ss 3336  df-sn 3822  df-iun 4097
  Copyright terms: Public domain W3C validator