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

Theorem uniiun 4295
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 4164 . 2  |-  U. A  =  { y  |  E. x  e.  A  y  e.  x }
2 df-iun 4244 . 2  |-  U_ x  e.  A  x  =  { y  |  E. x  e.  A  y  e.  x }
31, 2eqtr4i 2453 1  |-  U. A  =  U_ x  e.  A  x
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   {cab 2414   E.wrex 2715   U.cuni 4162   U_ciun 4242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-rex 2720  df-uni 4163  df-iun 4244
This theorem is referenced by:  iununi  4330  iunpwss  4335  truni  4475  reluni  4918  rnuni  5209  imauni  6110  iunpw  6563  oa0r  7195  om1r  7199  oeworde  7249  unifi  7816  infssuni  7818  cfslb2n  8649  ituniiun  8803  unidom  8919  unictb  8951  gruuni  9176  gruun  9182  hashuni  13827  tgidm  19938  unicld  20003  clsval2  20007  mretopd  20050  tgrest  20117  cmpsublem  20356  cmpsub  20357  tgcmp  20358  hauscmplem  20363  cmpfi  20365  uncon  20386  concompcon  20389  comppfsc  20489  kgentopon  20495  txbasval  20563  txtube  20597  txcmplem1  20598  txcmplem2  20599  xkococnlem  20616  alexsublem  21001  alexsubALT  21008  opnmblALT  22503  limcun  22792  uniin1  28110  uniin2  28111  disjuniel  28153  hashunif  28330  dmvlsiga  28903  measinblem  28994  volmeas  29006  carsggect  29102  omsmeas  29107  omsmeasOLD  29108  cvmscld  29948  istotbnd3  32010  sstotbnd  32014  heiborlem3  32052  heibor  32060  fiunicl  37324  founiiun  37350  founiiun0  37369  psmeasurelem  38159
  Copyright terms: Public domain W3C validator