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

Theorem uniiun 3853
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
StepHypRef Expression
1 dfuni2 3729 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
2 df-iun 3805 . 2  |-  U_ x  e.  A  x  =  { y  |  E. x  e.  A  y  e.  x }
31, 2eqtr4i 2276 1  |-  U. A  =  U_ x  e.  A  x
Colors of variables: wff set class
Syntax hints:    = wceq 1619    e. wcel 1621   {cab 2239   E.wrex 2510   U.cuni 3727   U_ciun 3803
This theorem is referenced by:  iununi  3884  iunpwss  3889  truni  4024  iunpw  4461  reluni  4715  rnuni  4999  imauni  5624  oa0r  6423  om1r  6427  oeworde  6477  unifi  7030  cfslb2n  7778  ituniiun  7932  unidom  8049  unictb  8077  gruuni  8302  gruun  8308  hashuni  12160  hashuniOLD  12161  tgidm  16550  unicld  16615  clsval2  16619  mretopd  16661  tgrest  16722  cmpsublem  16958  cmpsub  16959  tgcmp  16960  hauscmplem  16965  cmpfi  16967  uncon  16987  concompcon  16990  kgentopon  17065  txbasval  17133  txtube  17166  txcmplem1  17167  txcmplem2  17168  xkococnlem  17185  alexsublem  17570  alexsubALT  17577  opnmblALT  18790  limcun  19077  cvmscld  22975  isunscov  24239  comppfsc  25473  istotbnd3  25661  sstotbnd  25665  heiborlem3  25703  heibor  25711
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-rex 2514  df-uni 3728  df-iun 3805
  Copyright terms: Public domain W3C validator