Metamath Proof Explorer


Theorem imaiun

Description: The image of an indexed union is the indexed union of the images. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion imaiun
|- ( A " U_ x e. B C ) = U_ x e. B ( A " C )

Proof

Step Hyp Ref Expression
1 rexcom4
 |-  ( 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
 |-  y e. _V
3 2 elima3
 |-  ( y e. ( A " C ) <-> E. z ( z e. C /\ <. z , y >. e. A ) )
4 3 rexbii
 |-  ( E. x e. B y e. ( A " C ) <-> E. x e. B E. z ( z e. C /\ <. z , y >. e. A ) )
5 eliun
 |-  ( z e. U_ x e. B C <-> E. x e. B z e. C )
6 5 anbi1i
 |-  ( ( 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
 |-  ( E. x e. B ( z e. C /\ <. z , y >. e. A ) <-> ( E. x e. B z e. C /\ <. z , y >. e. A ) )
8 6 7 bitr4i
 |-  ( ( z e. U_ x e. B C /\ <. z , y >. e. A ) <-> E. x e. B ( z e. C /\ <. z , y >. e. A ) )
9 8 exbii
 |-  ( 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 ) )
10 1 4 9 3bitr4ri
 |-  ( E. z ( z e. U_ x e. B C /\ <. z , y >. e. A ) <-> E. x e. B y e. ( A " C ) )
11 2 elima3
 |-  ( y e. ( A " U_ x e. B C ) <-> E. z ( z e. U_ x e. B C /\ <. z , y >. e. A ) )
12 eliun
 |-  ( y e. U_ x e. B ( A " C ) <-> E. x e. B y e. ( A " C ) )
13 10 11 12 3bitr4i
 |-  ( y e. ( A " U_ x e. B C ) <-> y e. U_ x e. B ( A " C ) )
14 13 eqriv
 |-  ( A " U_ x e. B C ) = U_ x e. B ( A " C )