This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )