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

Theorem imaiun 5957
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 2987 . . . 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 2970 . . . . . 6  |-  y  e. 
_V
32elima3 5171 . . . . 5  |-  ( y  e.  ( A " C )  <->  E. z
( z  e.  C  /\  <. z ,  y
>.  e.  A ) )
43rexbii 2735 . . . 4  |-  ( E. x  e.  B  y  e.  ( A " C )  <->  E. x  e.  B  E. z
( z  e.  C  /\  <. z ,  y
>.  e.  A ) )
5 eliun 4170 . . . . . . 7  |-  ( z  e.  U_ x  e.  B  C  <->  E. x  e.  B  z  e.  C )
65anbi1i 695 . . . . . 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 2868 . . . . . 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 252 . . . . 5  |-  ( ( z  e.  U_ x  e.  B  C  /\  <.
z ,  y >.  e.  A )  <->  E. x  e.  B  ( z  e.  C  /\  <. z ,  y >.  e.  A
) )
98exbii 1634 . . . 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 278 . . 3  |-  ( E. z ( z  e. 
U_ x  e.  B  C  /\  <. z ,  y
>.  e.  A )  <->  E. x  e.  B  y  e.  ( A " C ) )
112elima3 5171 . . 3  |-  ( y  e.  ( A " U_ x  e.  B  C )  <->  E. z
( z  e.  U_ x  e.  B  C  /\  <. z ,  y
>.  e.  A ) )
12 eliun 4170 . . 3  |-  ( y  e.  U_ x  e.  B  ( A " C )  <->  E. x  e.  B  y  e.  ( A " C ) )
1310, 11, 123bitr4i 277 . 2  |-  ( y  e.  ( A " U_ x  e.  B  C )  <->  y  e.  U_ x  e.  B  ( A " C ) )
1413eqriv 2435 1  |-  ( A
" U_ x  e.  B  C )  =  U_ x  e.  B  ( A " C )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1369   E.wex 1586    e. wcel 1756   E.wrex 2711   <.cop 3878   U_ciun 4166   "cima 4838
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-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-iun 4168  df-br 4288  df-opab 4346  df-xp 4841  df-cnv 4843  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848
This theorem is referenced by:  imauni  5958  uniqs  7152  hsmexlem4  8590  hsmexlem5  8591  xkococnlem  19212  ismbf3d  21112  mbfimaopnlem  21113  i1fima  21136  i1fd  21139  itg1addlem5  21158  limciun  21349  sibfof  26695  eulerpartlemgh  26730  itg2addnclem2  28415  ftc1anclem6  28443
  Copyright terms: Public domain W3C validator