imaundir

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

		Ref	Expression
	Assertion	imaundir	$⊢ (A \cup B) [C] = A [C] \cup B [C]$

Step	Hyp	Ref	Expression
1		df-ima	$⊢ (A \cup B) [C] = ran ({(A \cup B) ↾}_{C})$
2		resundir	$⊢ {(A \cup B) ↾}_{C} = ({A ↾}_{C}) \cup ({B ↾}_{C})$
3	2	rneqi	$⊢ ran ({(A \cup B) ↾}_{C}) = ran (({A ↾}_{C}) \cup ({B ↾}_{C}))$
4		rnun	$⊢ ran (({A ↾}_{C}) \cup ({B ↾}_{C})) = ran ({A ↾}_{C}) \cup ran ({B ↾}_{C})$
5	1 3 4	3eqtri	$⊢ (A \cup B) [C] = ran ({A ↾}_{C}) \cup 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] \cup B [C] = ran ({A ↾}_{C}) \cup ran ({B ↾}_{C})$
9	5 8	eqtr4i	$⊢ (A \cup B) [C] = A [C] \cup B [C]$

Metamath Proof Explorer