Theorem 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 \left({\mathrm{I}\upharpoonright }_A\right)\left[B\right]=B$$

Proof

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