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

Theorem uniiun 4104
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 3977 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
2 df-iun 4055 . 2  |-  U_ x  e.  A  x  =  { y  |  E. x  e.  A  y  e.  x }
31, 2eqtr4i 2427 1  |-  U. A  =  U_ x  e.  A  x
Colors of variables: wff set class
Syntax hints:    = wceq 1649   {cab 2390   E.wrex 2667   U.cuni 3975   U_ciun 4053
This theorem is referenced by:  iununi  4135  iunpwss  4140  truni  4276  iunpw  4718  reluni  4956  rnuni  5242  imauni  5952  oa0r  6741  om1r  6745  oeworde  6795  unifi  7354  cfslb2n  8104  ituniiun  8258  unidom  8374  unictb  8406  gruuni  8631  gruun  8637  hashuni  12559  hashuniOLD  12560  tgidm  17000  unicld  17065  clsval2  17069  mretopd  17111  tgrest  17177  cmpsublem  17416  cmpsub  17417  tgcmp  17418  hauscmplem  17423  cmpfi  17425  uncon  17445  concompcon  17448  kgentopon  17523  txbasval  17591  txtube  17625  txcmplem1  17626  txcmplem2  17627  xkococnlem  17644  alexsublem  18028  alexsubALT  18035  opnmblALT  19448  limcun  19735  hashunif  24111  dmvlsiga  24465  measinblem  24527  volmeas  24540  cvmscld  24913  comppfsc  26277  istotbnd3  26370  sstotbnd  26374  heiborlem3  26412  heibor  26420
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-rex 2672  df-uni 3976  df-iun 4055
  Copyright terms: Public domain W3C validator