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

Theorem iunxun 4376
Description: Separate a union in the index of an indexed union. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
Assertion
Ref Expression
iunxun  |-  U_ x  e.  ( A  u.  B
) C  =  (
U_ x  e.  A  C  u.  U_ x  e.  B  C )

Proof of Theorem iunxun
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 rexun 3625 . . . 4  |-  ( E. x  e.  ( A  u.  B ) y  e.  C  <->  ( E. x  e.  A  y  e.  C  \/  E. x  e.  B  y  e.  C ) )
2 eliun 4296 . . . . 5  |-  ( y  e.  U_ x  e.  A  C  <->  E. x  e.  A  y  e.  C )
3 eliun 4296 . . . . 5  |-  ( y  e.  U_ x  e.  B  C  <->  E. x  e.  B  y  e.  C )
42, 3orbi12i 528 . . . 4  |-  ( ( y  e.  U_ x  e.  A  C  \/  y  e.  U_ x  e.  B  C )  <->  ( E. x  e.  A  y  e.  C  \/  E. x  e.  B  y  e.  C ) )
51, 4bitr4i 260 . . 3  |-  ( E. x  e.  ( A  u.  B ) y  e.  C  <->  ( y  e.  U_ x  e.  A  C  \/  y  e.  U_ x  e.  B  C
) )
6 eliun 4296 . . 3  |-  ( y  e.  U_ x  e.  ( A  u.  B
) C  <->  E. x  e.  ( A  u.  B
) y  e.  C
)
7 elun 3585 . . 3  |-  ( y  e.  ( U_ x  e.  A  C  u.  U_ x  e.  B  C
)  <->  ( y  e. 
U_ x  e.  A  C  \/  y  e.  U_ x  e.  B  C
) )
85, 6, 73bitr4i 285 . 2  |-  ( y  e.  U_ x  e.  ( A  u.  B
) C  <->  y  e.  ( U_ x  e.  A  C  u.  U_ x  e.  B  C ) )
98eqriv 2458 1  |-  U_ x  e.  ( A  u.  B
) C  =  (
U_ x  e.  A  C  u.  U_ x  e.  B  C )
Colors of variables: wff setvar class
Syntax hints:    \/ wo 374    = wceq 1454    e. wcel 1897   E.wrex 2749    u. cun 3413   U_ciun 4291
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-rex 2754  df-v 3058  df-un 3420  df-iun 4293
This theorem is referenced by:  iunsuc  5523  funiunfv  6177  iunfi  7887  kmlem11  8615  ackbij1lem9  8683  fsum2dlem  13879  fsumiun  13929  fprod2dlem  14082  prmreclem4  14911  fiuncmp  20467  ovolfiniun  22502  finiunmbl  22545  volfiniun  22548  voliunlem1  22551  uniioombllem4  22592  iunxdif3  28223  iuninc  28224  ofpreima2  28317  indval2  28884  esum2dlem  28961  sigaclfu2  28991  fiunelros  29044  measvuni  29084  cvmliftlem10  30065  mrsubvrs  30208  mblfinlem2  32022  dfrcl4  36312  iunrelexp0  36338  comptiunov2i  36342  corclrcl  36343  trclfvdecomr  36364  dfrtrcl4  36374  corcltrcl  36375  cotrclrcl  36378  fiiuncl  37443  iunp1  37444  sge0iunmptlemfi  38292  iunxprg  39043
  Copyright terms: Public domain W3C validator