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

Theorem uniiun 3971
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 3845 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
2 df-iun 3923 . 2  |-  U_ x  e.  A  x  =  { y  |  E. x  e.  A  y  e.  x }
31, 2eqtr4i 2319 1  |-  U. A  =  U_ x  e.  A  x
Colors of variables: wff set class
Syntax hints:    = wceq 1632    e. wcel 1696   {cab 2282   E.wrex 2557   U.cuni 3843   U_ciun 3921
This theorem is referenced by:  iununi  4002  iunpwss  4007  truni  4143  iunpw  4586  reluni  4824  rnuni  5108  imauni  5788  oa0r  6553  om1r  6557  oeworde  6607  unifi  7161  cfslb2n  7910  ituniiun  8064  unidom  8181  unictb  8213  gruuni  8438  gruun  8444  hashuni  12299  hashuniOLD  12300  tgidm  16734  unicld  16799  clsval2  16803  mretopd  16845  tgrest  16906  cmpsublem  17142  cmpsub  17143  tgcmp  17144  hauscmplem  17149  cmpfi  17151  uncon  17171  concompcon  17174  kgentopon  17249  txbasval  17317  txtube  17350  txcmplem1  17351  txcmplem2  17352  xkococnlem  17369  alexsublem  17754  alexsubALT  17761  opnmblALT  18974  limcun  19261  hashunif  23400  dmvlsiga  23505  measinblem  23562  cvmscld  23819  isunscov  25177  comppfsc  26410  istotbnd3  26598  sstotbnd  26602  heiborlem3  26640  heibor  26648
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-rex 2562  df-uni 3844  df-iun 3923
  Copyright terms: Public domain W3C validator