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

Theorem uniiun 3955
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 3829 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
2 df-iun 3907 . 2  |-  U_ x  e.  A  x  =  { y  |  E. x  e.  A  y  e.  x }
31, 2eqtr4i 2306 1  |-  U. A  =  U_ x  e.  A  x
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684   {cab 2269   E.wrex 2544   U.cuni 3827   U_ciun 3905
This theorem is referenced by:  iununi  3986  iunpwss  3991  truni  4127  iunpw  4570  reluni  4808  rnuni  5092  imauni  5772  oa0r  6537  om1r  6541  oeworde  6591  unifi  7145  cfslb2n  7894  ituniiun  8048  unidom  8165  unictb  8197  gruuni  8422  gruun  8428  hashuni  12283  hashuniOLD  12284  tgidm  16718  unicld  16783  clsval2  16787  mretopd  16829  tgrest  16890  cmpsublem  17126  cmpsub  17127  tgcmp  17128  hauscmplem  17133  cmpfi  17135  uncon  17155  concompcon  17158  kgentopon  17233  txbasval  17301  txtube  17334  txcmplem1  17335  txcmplem2  17336  xkococnlem  17353  alexsublem  17738  alexsubALT  17745  opnmblALT  18958  limcun  19245  hashunif  23385  dmvlsiga  23490  measinblem  23547  cvmscld  23804  isunscov  25074  comppfsc  26307  istotbnd3  26495  sstotbnd  26499  heiborlem3  26537  heibor  26545
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-rex 2549  df-uni 3828  df-iun 3907
  Copyright terms: Public domain W3C validator