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

Theorem imaiun 6136
Description: The image of an indexed union is the indexed union of the images. (Contributed by Mario Carneiro, 18-Jun-2014.)
Assertion
Ref Expression
imaiun  |-  ( A
" U_ x  e.  B  C )  =  U_ x  e.  B  ( A " C )
Distinct variable group:    x, A
Allowed substitution hints:    B( x)    C( x)

Proof of Theorem imaiun
Dummy variables  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rexcom4 3035 . . . 4  |-  ( E. x  e.  B  E. z ( z  e.  C  /\  <. z ,  y >.  e.  A
)  <->  E. z E. x  e.  B  ( z  e.  C  /\  <. z ,  y >.  e.  A
) )
2 vex 3016 . . . . . 6  |-  y  e. 
_V
32elima3 5153 . . . . 5  |-  ( y  e.  ( A " C )  <->  E. z
( z  e.  C  /\  <. z ,  y
>.  e.  A ) )
43rexbii 2862 . . . 4  |-  ( E. x  e.  B  y  e.  ( A " C )  <->  E. x  e.  B  E. z
( z  e.  C  /\  <. z ,  y
>.  e.  A ) )
5 eliun 4253 . . . . . . 7  |-  ( z  e.  U_ x  e.  B  C  <->  E. x  e.  B  z  e.  C )
65anbi1i 706 . . . . . 6  |-  ( ( z  e.  U_ x  e.  B  C  /\  <.
z ,  y >.  e.  A )  <->  ( E. x  e.  B  z  e.  C  /\  <. z ,  y >.  e.  A
) )
7 r19.41v 2910 . . . . . 6  |-  ( E. x  e.  B  ( z  e.  C  /\  <.
z ,  y >.  e.  A )  <->  ( E. x  e.  B  z  e.  C  /\  <. z ,  y >.  e.  A
) )
86, 7bitr4i 260 . . . . 5  |-  ( ( z  e.  U_ x  e.  B  C  /\  <.
z ,  y >.  e.  A )  <->  E. x  e.  B  ( z  e.  C  /\  <. z ,  y >.  e.  A
) )
98exbii 1722 . . . 4  |-  ( E. z ( z  e. 
U_ x  e.  B  C  /\  <. z ,  y
>.  e.  A )  <->  E. z E. x  e.  B  ( z  e.  C  /\  <. z ,  y
>.  e.  A ) )
101, 4, 93bitr4ri 286 . . 3  |-  ( E. z ( z  e. 
U_ x  e.  B  C  /\  <. z ,  y
>.  e.  A )  <->  E. x  e.  B  y  e.  ( A " C ) )
112elima3 5153 . . 3  |-  ( y  e.  ( A " U_ x  e.  B  C )  <->  E. z
( z  e.  U_ x  e.  B  C  /\  <. z ,  y
>.  e.  A ) )
12 eliun 4253 . . 3  |-  ( y  e.  U_ x  e.  B  ( A " C )  <->  E. x  e.  B  y  e.  ( A " C ) )
1310, 11, 123bitr4i 285 . 2  |-  ( y  e.  ( A " U_ x  e.  B  C )  <->  y  e.  U_ x  e.  B  ( A " C ) )
1413eqriv 2449 1  |-  ( A
" U_ x  e.  B  C )  =  U_ x  e.  B  ( A " C )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 375    = wceq 1448   E.wex 1667    e. wcel 1891   E.wrex 2738   <.cop 3942   U_ciun 4248   "cima 4815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pr 4612
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3015  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-iun 4250  df-br 4375  df-opab 4434  df-xp 4818  df-cnv 4820  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825
This theorem is referenced by:  imauni  6137  uniqs  7410  hsmexlem4  8846  hsmexlem5  8847  xkococnlem  20685  ismbf3d  22622  mbfimaopnlem  22623  i1fima  22648  i1fd  22651  itg1addlem5  22670  limciun  22861  sibfof  29179  eulerpartlemgh  29217  poimirlem30  31972  itg2addnclem2  31996  ftc1anclem6  32024
  Copyright terms: Public domain W3C validator