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

Theorem uniiun 4244
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 4114 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
2 df-iun 4194 . 2  |-  U_ x  e.  A  x  =  { y  |  E. x  e.  A  y  e.  x }
31, 2eqtr4i 2466 1  |-  U. A  =  U_ x  e.  A  x
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369   {cab 2429   E.wrex 2737   U.cuni 4112   U_ciun 4192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-rex 2742  df-uni 4113  df-iun 4194
This theorem is referenced by:  iununi  4276  iunpwss  4281  truni  4420  reluni  4983  rnuni  5269  imauni  5984  iunpw  6411  oa0r  6999  om1r  7003  oeworde  7053  unifi  7621  infssuni  7623  cfslb2n  8458  ituniiun  8612  unidom  8728  unictb  8760  gruuni  8988  gruun  8994  hashuni  13309  hashuniOLD  13310  tgidm  18607  unicld  18672  clsval2  18676  mretopd  18718  tgrest  18785  cmpsublem  19024  cmpsub  19025  tgcmp  19026  hauscmplem  19031  cmpfi  19033  uncon  19055  concompcon  19058  kgentopon  19133  txbasval  19201  txtube  19235  txcmplem1  19236  txcmplem2  19237  xkococnlem  19254  alexsublem  19638  alexsubALT  19645  opnmblALT  21105  limcun  21392  hashunif  26106  dmvlsiga  26594  measinblem  26656  volmeas  26669  cvmscld  27184  comppfsc  28605  istotbnd3  28696  sstotbnd  28700  heiborlem3  28738  heibor  28746
  Copyright terms: Public domain W3C validator