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

Theorem uniiun 4344
Description: Class union in terms of indexed union. Definition in [Stoll] p. 43. (Contributed by NM, 28-Jun-1998.)
Assertion
Ref Expression
uniiun  |-  U. A  =  U_ x  e.  A  x
Distinct variable group:    x, A

Proof of Theorem uniiun
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dfuni2 4213 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
2 df-iun 4293 . 2  |-  U_ x  e.  A  x  =  { y  |  E. x  e.  A  y  e.  x }
31, 2eqtr4i 2486 1  |-  U. A  =  U_ x  e.  A  x
Colors of variables: wff setvar class
Syntax hints:    = wceq 1454   {cab 2447   E.wrex 2749   U.cuni 4211   U_ciun 4291
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-rex 2754  df-uni 4212  df-iun 4293
This theorem is referenced by:  iununi  4379  iunpwss  4384  truni  4524  reluni  4974  rnuni  5265  imauni  6175  iunpw  6631  oa0r  7265  om1r  7269  oeworde  7319  unifi  7888  infssuni  7890  cfslb2n  8723  ituniiun  8877  unidom  8993  unictb  9025  gruuni  9250  gruun  9256  hashuni  13932  tgidm  20044  unicld  20109  clsval2  20113  mretopd  20156  tgrest  20223  cmpsublem  20462  cmpsub  20463  tgcmp  20464  hauscmplem  20469  cmpfi  20471  uncon  20492  concompcon  20495  comppfsc  20595  kgentopon  20601  txbasval  20669  txtube  20703  txcmplem1  20704  txcmplem2  20705  xkococnlem  20722  alexsublem  21107  alexsubALT  21114  opnmblALT  22609  limcun  22898  uniin1  28212  uniin2  28213  disjuniel  28255  hashunif  28427  dmvlsiga  28999  measinblem  29090  volmeas  29102  carsggect  29198  omsmeas  29203  omsmeasOLD  29204  cvmscld  30044  istotbnd3  32147  sstotbnd  32151  heiborlem3  32189  heibor  32197  fiunicl  37445  founiiun  37483  founiiun0  37502  psmeasurelem  38345
  Copyright terms: Public domain W3C validator