Theorem resima2

Description: Image under a restricted class. (Contributed by FL, 31-Aug-2009) (Proof shortened by JJ, 25-Aug-2021)

	Ref	Expression
Assertion	resima2	$$⊢B\subseteq C\to \left({A\upharpoonright }_C\right)\left[B\right]=A\left[B\right]$$

Proof

Step	Hyp	Ref	Expression
1		sseqin2	$$⊢B\subseteq C\leftrightarrow C\cap B=B$$
2		reseq2	$$⊢C\cap B=B\to {A\upharpoonright }_{\left(C\cap B\right)}={A\upharpoonright }_B$$
3	1 2	sylbi	$$⊢B\subseteq C\to {A\upharpoonright }_{\left(C\cap B\right)}={A\upharpoonright }_B$$
4	3	rneqd	$$⊢B\subseteq C\to \mathrm{ran}\left({A\upharpoonright }_{\left(C\cap B\right)}\right)=\mathrm{ran}\left({A\upharpoonright }_B\right)$$
5		df-ima	$$⊢\left({A\upharpoonright }_C\right)\left[B\right]=\mathrm{ran}\left({\left({A\upharpoonright }_C\right)\upharpoonright }_B\right)$$
6		resres	$$⊢{\left({A\upharpoonright }_C\right)\upharpoonright }_B={A\upharpoonright }_{\left(C\cap B\right)}$$
7	6	rneqi	$$⊢\mathrm{ran}\left({\left({A\upharpoonright }_C\right)\upharpoonright }_B\right)=\mathrm{ran}\left({A\upharpoonright }_{\left(C\cap B\right)}\right)$$
8	5 7	eqtri	$$⊢\left({A\upharpoonright }_C\right)\left[B\right]=\mathrm{ran}\left({A\upharpoonright }_{\left(C\cap B\right)}\right)$$
9		df-ima	$$⊢A\left[B\right]=\mathrm{ran}\left({A\upharpoonright }_B\right)$$
10	4 8 9	3eqtr4g	$$⊢B\subseteq C\to \left({A\upharpoonright }_C\right)\left[B\right]=A\left[B\right]$$