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

Theorem uniiun 3915
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 3789 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
2 df-iun 3867 . 2  |-  U_ x  e.  A  x  =  { y  |  E. x  e.  A  y  e.  x }
31, 2eqtr4i 2279 1  |-  U. A  =  U_ x  e.  A  x
Colors of variables: wff set class
Syntax hints:    = wceq 1619    e. wcel 1621   {cab 2242   E.wrex 2517   U.cuni 3787   U_ciun 3865
This theorem is referenced by:  iununi  3946  iunpwss  3951  truni  4087  iunpw  4528  reluni  4782  rnuni  5066  imauni  5692  oa0r  6491  om1r  6495  oeworde  6545  unifi  7099  cfslb2n  7848  ituniiun  8002  unidom  8119  unictb  8151  gruuni  8376  gruun  8382  hashuni  12234  hashuniOLD  12235  tgidm  16666  unicld  16731  clsval2  16735  mretopd  16777  tgrest  16838  cmpsublem  17074  cmpsub  17075  tgcmp  17076  hauscmplem  17081  cmpfi  17083  uncon  17103  concompcon  17106  kgentopon  17181  txbasval  17249  txtube  17282  txcmplem1  17283  txcmplem2  17284  xkococnlem  17301  alexsublem  17686  alexsubALT  17693  opnmblALT  18906  limcun  19193  cvmscld  23162  isunscov  24426  comppfsc  25660  istotbnd3  25848  sstotbnd  25852  heiborlem3  25890  heibor  25898
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 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-rex 2522  df-uni 3788  df-iun 3867
  Copyright terms: Public domain W3C validator