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

Theorem uniiun 4368
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 4237 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
2 df-iun 4317 . 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 1398   {cab 2439   E.wrex 2805   U.cuni 4235   U_ciun 4315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-rex 2810  df-uni 4236  df-iun 4317
This theorem is referenced by:  iununi  4403  iunpwss  4408  truni  4546  reluni  5113  rnuni  5402  imauni  6133  iunpw  6587  oa0r  7180  om1r  7184  oeworde  7234  unifi  7801  infssuni  7803  cfslb2n  8639  ituniiun  8793  unidom  8909  unictb  8941  gruuni  9167  gruun  9173  hashuni  13723  tgidm  19652  unicld  19717  clsval2  19721  mretopd  19763  tgrest  19830  cmpsublem  20069  cmpsub  20070  tgcmp  20071  hauscmplem  20076  cmpfi  20078  uncon  20099  concompcon  20102  comppfsc  20202  kgentopon  20208  txbasval  20276  txtube  20310  txcmplem1  20311  txcmplem2  20312  xkococnlem  20329  alexsublem  20713  alexsubALT  20720  opnmblALT  22181  limcun  22468  disjuniel  27670  hashunif  27842  dmvlsiga  28362  measinblem  28431  volmeas  28443  carsggect  28529  omsmeas  28534  cvmscld  28985  istotbnd3  30510  sstotbnd  30514  heiborlem3  30552  heibor  30560
  Copyright terms: Public domain W3C validator