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

Theorem iunid 4297
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 3942 . . . . 5  |-  { x }  =  { y  |  y  =  x }
2 equcom 1848 . . . . . 6  |-  ( y  =  x  <->  x  =  y )
32abbii 2544 . . . . 5  |-  { y  |  y  =  x }  =  { y  |  x  =  y }
41, 3eqtri 2450 . . . 4  |-  { x }  =  { y  |  x  =  y }
54a1i 11 . . 3  |-  ( x  e.  A  ->  { x }  =  { y  |  x  =  y } )
65iuneq2i 4261 . 2  |-  U_ x  e.  A  { x }  =  U_ x  e.  A  { y  |  x  =  y }
7 iunab 4288 . . 3  |-  U_ x  e.  A  { y  |  x  =  y }  =  { y  |  E. x  e.  A  x  =  y }
8 risset 2892 . . . 4  |-  ( y  e.  A  <->  E. x  e.  A  x  =  y )
98abbii 2544 . . 3  |-  { y  |  y  e.  A }  =  { y  |  E. x  e.  A  x  =  y }
10 abid2 2550 . . 3  |-  { y  |  y  e.  A }  =  A
117, 9, 103eqtr2i 2456 . 2  |-  U_ x  e.  A  { y  |  x  =  y }  =  A
126, 11eqtri 2450 1  |-  U_ x  e.  A  { x }  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1872   {cab 2414   E.wrex 2715   {csn 3941   U_ciun 4242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ral 2719  df-rex 2720  df-v 3024  df-in 3386  df-ss 3393  df-sn 3942  df-iun 4244
This theorem is referenced by:  iunxpconst  4853  fvn0ssdmfun  5972  xpexgALT  6744  uniqs  7378  rankcf  9153  dprd2da  17618  t1ficld  20285  discmp  20355  xkoinjcn  20644  metnrmlem2  21819  metnrmlem2OLD  21834  ovoliunlem1  22397  i1fima  22578  i1fd  22581  itg1addlem5  22600  sibfof  29125  bnj1415  29799  cvmlift2lem12  29989  dftrpred4g  30426  poimirlem30  31877  itg2addnclem2  31901  ftc1anclem6  31929
  Copyright terms: Public domain W3C validator