Theorem imaiun1

Description: The image of an indexed union is the indexed union of the images. (Contributed by RP, 29-Jun-2020)

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

Proof

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