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

Theorem iunid 4373
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 4021 . . . . 5  |-  { x }  =  { y  |  y  =  x }
2 equcom 1738 . . . . . 6  |-  ( y  =  x  <->  x  =  y )
32abbii 2594 . . . . 5  |-  { y  |  y  =  x }  =  { y  |  x  =  y }
41, 3eqtri 2489 . . . 4  |-  { x }  =  { y  |  x  =  y }
54a1i 11 . . 3  |-  ( x  e.  A  ->  { x }  =  { y  |  x  =  y } )
65iuneq2i 4337 . 2  |-  U_ x  e.  A  { x }  =  U_ x  e.  A  { y  |  x  =  y }
7 iunab 4364 . . 3  |-  U_ x  e.  A  { y  |  x  =  y }  =  { y  |  E. x  e.  A  x  =  y }
8 risset 2980 . . . 4  |-  ( y  e.  A  <->  E. x  e.  A  x  =  y )
98abbii 2594 . . 3  |-  { y  |  y  e.  A }  =  { y  |  E. x  e.  A  x  =  y }
10 abid2 2600 . . 3  |-  { y  |  y  e.  A }  =  A
117, 9, 103eqtr2i 2495 . 2  |-  U_ x  e.  A  { y  |  x  =  y }  =  A
126, 11eqtri 2489 1  |-  U_ x  e.  A  { x }  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374    e. wcel 1762   {cab 2445   E.wrex 2808   {csn 4020   U_ciun 4318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rex 2813  df-v 3108  df-in 3476  df-ss 3483  df-sn 4021  df-iun 4320
This theorem is referenced by:  iunxpconst  5048  xpexgALT  6767  uniqs  7361  rankcf  9144  dprd2da  16874  t1ficld  19587  discmp  19657  xkoinjcn  19916  metnrmlem2  21092  ovoliunlem1  21641  i1fima  21813  i1fd  21816  itg1addlem5  21835  sibfof  27772  cvmlift2lem12  28249  dftrpred4g  28744  itg2addnclem2  29495  ftc1anclem6  29523  bnj1415  33048
  Copyright terms: Public domain W3C validator