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 )