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

Theorem uniiun 4378
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 4247 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
2 df-iun 4327 . 2  |-  U_ x  e.  A  x  =  { y  |  E. x  e.  A  y  e.  x }
31, 2eqtr4i 2499 1  |-  U. A  =  U_ x  e.  A  x
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379   {cab 2452   E.wrex 2815   U.cuni 4245   U_ciun 4325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-rex 2820  df-uni 4246  df-iun 4327
This theorem is referenced by:  iununi  4410  iunpwss  4415  truni  4554  reluni  5125  rnuni  5417  imauni  6147  iunpw  6599  oa0r  7189  om1r  7193  oeworde  7243  unifi  7810  infssuni  7812  cfslb2n  8649  ituniiun  8803  unidom  8919  unictb  8951  gruuni  9179  gruun  9185  hashuni  13604  tgidm  19288  unicld  19353  clsval2  19357  mretopd  19399  tgrest  19466  cmpsublem  19705  cmpsub  19706  tgcmp  19707  hauscmplem  19712  cmpfi  19714  uncon  19736  concompcon  19739  comppfsc  19860  kgentopon  19866  txbasval  19934  txtube  19968  txcmplem1  19969  txcmplem2  19970  xkococnlem  19987  alexsublem  20371  alexsubALT  20378  opnmblALT  21839  limcun  22126  hashunif  27370  dmvlsiga  27880  measinblem  27942  volmeas  27954  cvmscld  28469  istotbnd3  30097  sstotbnd  30101  heiborlem3  30139  heibor  30147
  Copyright terms: Public domain W3C validator