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

Theorem iunid 3957
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 3646 . . . . 5  |-  { x }  =  { y  |  y  =  x }
2 equcom 1647 . . . . . 6  |-  ( y  =  x  <->  x  =  y )
32abbii 2395 . . . . 5  |-  { y  |  y  =  x }  =  { y  |  x  =  y }
41, 3eqtri 2303 . . . 4  |-  { x }  =  { y  |  x  =  y }
54a1i 10 . . 3  |-  ( x  e.  A  ->  { x }  =  { y  |  x  =  y } )
65iuneq2i 3923 . 2  |-  U_ x  e.  A  { x }  =  U_ x  e.  A  { y  |  x  =  y }
7 iunab 3948 . . 3  |-  U_ x  e.  A  { y  |  x  =  y }  =  { y  |  E. x  e.  A  x  =  y }
8 risset 2590 . . . 4  |-  ( y  e.  A  <->  E. x  e.  A  x  =  y )
98abbii 2395 . . 3  |-  { y  |  y  e.  A }  =  { y  |  E. x  e.  A  x  =  y }
10 abid2 2400 . . 3  |-  { y  |  y  e.  A }  =  A
117, 9, 103eqtr2i 2309 . 2  |-  U_ x  e.  A  { y  |  x  =  y }  =  A
126, 11eqtri 2303 1  |-  U_ x  e.  A  { x }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684   {cab 2269   E.wrex 2544   {csn 3640   U_ciun 3905
This theorem is referenced by:  iunxpconst  4746  xpexgALT  6070  uniqs  6719  rankcf  8399  dprd2da  15277  t1ficld  17055  discmp  17125  xkoinjcn  17381  metnrmlem2  18364  ovoliunlem1  18861  i1fima  19033  i1fd  19036  itg1addlem5  19055  cvmlift2lem12  23845  dftrpred4g  24237  bnj1415  29068
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-v 2790  df-in 3159  df-ss 3166  df-sn 3646  df-iun 3907
  Copyright terms: Public domain W3C validator