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

Theorem uniiun 4136
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 4009 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
2 df-iun 4087 . 2  |-  U_ x  e.  A  x  =  { y  |  E. x  e.  A  y  e.  x }
31, 2eqtr4i 2458 1  |-  U. A  =  U_ x  e.  A  x
Colors of variables: wff set class
Syntax hints:    = wceq 1652   {cab 2421   E.wrex 2698   U.cuni 4007   U_ciun 4085
This theorem is referenced by:  iununi  4167  iunpwss  4172  truni  4308  iunpw  4750  reluni  4988  rnuni  5274  imauni  5984  oa0r  6773  om1r  6777  oeworde  6827  unifi  7386  infssuni  7388  cfslb2n  8137  ituniiun  8291  unidom  8407  unictb  8439  gruuni  8664  gruun  8670  hashuni  12592  hashuniOLD  12593  tgidm  17033  unicld  17098  clsval2  17102  mretopd  17144  tgrest  17211  cmpsublem  17450  cmpsub  17451  tgcmp  17452  hauscmplem  17457  cmpfi  17459  uncon  17480  concompcon  17483  kgentopon  17558  txbasval  17626  txtube  17660  txcmplem1  17661  txcmplem2  17662  xkococnlem  17679  alexsublem  18063  alexsubALT  18070  opnmblALT  19483  limcun  19770  hashunif  24146  dmvlsiga  24500  measinblem  24562  volmeas  24575  cvmscld  24948  comppfsc  26324  istotbnd3  26417  sstotbnd  26421  heiborlem3  26459  heibor  26467
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-rex 2703  df-uni 4008  df-iun 4087
  Copyright terms: Public domain W3C validator