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

Theorem uniiun 4220
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 4090 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
2 df-iun 4170 . 2  |-  U_ x  e.  A  x  =  { y  |  E. x  e.  A  y  e.  x }
31, 2eqtr4i 2464 1  |-  U. A  =  U_ x  e.  A  x
Colors of variables: wff setvar class
Syntax hints:    = wceq 1364   {cab 2427   E.wrex 2714   U.cuni 4088   U_ciun 4168
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-rex 2719  df-uni 4089  df-iun 4170
This theorem is referenced by:  iununi  4252  iunpwss  4257  truni  4396  reluni  4958  rnuni  5245  imauni  5960  iunpw  6389  oa0r  6974  om1r  6978  oeworde  7028  unifi  7596  infssuni  7598  cfslb2n  8433  ituniiun  8587  unidom  8703  unictb  8735  gruuni  8963  gruun  8969  hashuni  13284  hashuniOLD  13285  tgidm  18544  unicld  18609  clsval2  18613  mretopd  18655  tgrest  18722  cmpsublem  18961  cmpsub  18962  tgcmp  18963  hauscmplem  18968  cmpfi  18970  uncon  18992  concompcon  18995  kgentopon  19070  txbasval  19138  txtube  19172  txcmplem1  19173  txcmplem2  19174  xkococnlem  19191  alexsublem  19575  alexsubALT  19582  opnmblALT  21042  limcun  21329  hashunif  26017  dmvlsiga  26508  measinblem  26570  volmeas  26583  cvmscld  27092  comppfsc  28504  istotbnd3  28595  sstotbnd  28599  heiborlem3  28637  heibor  28645
  Copyright terms: Public domain W3C validator