Theorem imaundir

Description: The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008)

	Ref	Expression
Assertion	imaundir	|- ( ( A u. B ) " C ) = ( ( A " C ) u. ( B " C ) )

Proof

Step	Hyp	Ref	Expression
1		df-ima	|- ( ( A u. B ) " C ) = ran ( ( A u. B ) |` C )
2		resundir	|- ( ( A u. B ) |` C ) = ( ( A |` C ) u. ( B |` C ) )
3	2	rneqi	|- ran ( ( A u. B ) |` C ) = ran ( ( A |` C ) u. ( B |` C ) )
4		rnun	|- ran ( ( A |` C ) u. ( B |` C ) ) = ( ran ( A |` C ) u. ran ( B |` C ) )
5	1 3 4	3eqtri	|- ( ( A u. B ) " C ) = ( ran ( A |` C ) u. ran ( B |` C ) )
6		df-ima	|- ( A " C ) = ran ( A |` C )
7		df-ima	|- ( B " C ) = ran ( B |` C )
8	6 7	uneq12i	|- ( ( A " C ) u. ( B " C ) ) = ( ran ( A |` C ) u. ran ( B |` C ) )
9	5 8	eqtr4i	|- ( ( A u. B ) " C ) = ( ( A " C ) u. ( B " C ) )