resiima

Description: The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006)

		Ref	Expression
	Assertion	resiima	$⊢ B \subseteq A \to ({I ↾}_{A}) [B] = B$

Step	Hyp	Ref	Expression
1		df-ima	$⊢ ({I ↾}_{A}) [B] = ran ({({I ↾}_{A}) ↾}_{B})$
2	1	a1i	$⊢ B \subseteq A \to ({I ↾}_{A}) [B] = ran ({({I ↾}_{A}) ↾}_{B})$
3		resabs1	$⊢ B \subseteq A \to {({I ↾}_{A}) ↾}_{B} = {I ↾}_{B}$
4	3	rneqd	$⊢ B \subseteq A \to ran ({({I ↾}_{A}) ↾}_{B}) = ran ({I ↾}_{B})$
5		rnresi	$⊢ ran ({I ↾}_{B}) = B$
6	5	a1i	$⊢ B \subseteq A \to ran ({I ↾}_{B}) = B$
7	2 4 6	3eqtrd	$⊢ B \subseteq A \to ({I ↾}_{A}) [B] = B$

Metamath Proof Explorer