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

Theorem uniiun 3956
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
Dummy variable  y is distinct from all other variables.

Proof of Theorem uniiun
StepHypRef Expression
1 dfuni2 3830 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
2 df-iun 3908 . 2  |-  U_ x  e.  A  x  =  { y  |  E. x  e.  A  y  e.  x }
31, 2eqtr4i 2307 1  |-  U. A  =  U_ x  e.  A  x
Colors of variables: wff set class
Syntax hints:    = wceq 1624    e. wcel 1685   {cab 2270   E.wrex 2545   U.cuni 3828   U_ciun 3906
This theorem is referenced by:  iununi  3987  iunpwss  3992  truni  4128  iunpw  4569  reluni  4807  rnuni  5091  imauni  5733  oa0r  6532  om1r  6536  oeworde  6586  unifi  7140  cfslb2n  7889  ituniiun  8043  unidom  8160  unictb  8192  gruuni  8417  gruun  8423  hashuni  12277  hashuniOLD  12278  tgidm  16712  unicld  16777  clsval2  16781  mretopd  16823  tgrest  16884  cmpsublem  17120  cmpsub  17121  tgcmp  17122  hauscmplem  17127  cmpfi  17129  uncon  17149  concompcon  17152  kgentopon  17227  txbasval  17295  txtube  17328  txcmplem1  17329  txcmplem2  17330  xkococnlem  17347  alexsublem  17732  alexsubALT  17739  opnmblALT  18952  limcun  19239  cvmscld  23208  isunscov  24472  comppfsc  25706  istotbnd3  25894  sstotbnd  25898  heiborlem3  25936  heibor  25944
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-rex 2550  df-uni 3829  df-iun 3908
  Copyright terms: Public domain W3C validator