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	⊢ ( 𝐵 ⊆ 𝐶 → ( ( 𝐴 ↾ 𝐶 ) “ 𝐵 ) = ( 𝐴 “ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		sseqin2	⊢ ( 𝐵 ⊆ 𝐶 ↔ ( 𝐶 ∩ 𝐵 ) = 𝐵 )
2		reseq2	⊢ ( ( 𝐶 ∩ 𝐵 ) = 𝐵 → ( 𝐴 ↾ ( 𝐶 ∩ 𝐵 ) ) = ( 𝐴 ↾ 𝐵 ) )
3	1 2	sylbi	⊢ ( 𝐵 ⊆ 𝐶 → ( 𝐴 ↾ ( 𝐶 ∩ 𝐵 ) ) = ( 𝐴 ↾ 𝐵 ) )
4	3	rneqd	⊢ ( 𝐵 ⊆ 𝐶 → ran ( 𝐴 ↾ ( 𝐶 ∩ 𝐵 ) ) = ran ( 𝐴 ↾ 𝐵 ) )
5		df-ima	⊢ ( ( 𝐴 ↾ 𝐶 ) “ 𝐵 ) = ran ( ( 𝐴 ↾ 𝐶 ) ↾ 𝐵 )
6		resres	⊢ ( ( 𝐴 ↾ 𝐶 ) ↾ 𝐵 ) = ( 𝐴 ↾ ( 𝐶 ∩ 𝐵 ) )
7	6	rneqi	⊢ ran ( ( 𝐴 ↾ 𝐶 ) ↾ 𝐵 ) = ran ( 𝐴 ↾ ( 𝐶 ∩ 𝐵 ) )
8	5 7	eqtri	⊢ ( ( 𝐴 ↾ 𝐶 ) “ 𝐵 ) = ran ( 𝐴 ↾ ( 𝐶 ∩ 𝐵 ) )
9		df-ima	⊢ ( 𝐴 “ 𝐵 ) = ran ( 𝐴 ↾ 𝐵 )
10	4 8 9	3eqtr4g	⊢ ( 𝐵 ⊆ 𝐶 → ( ( 𝐴 ↾ 𝐶 ) “ 𝐵 ) = ( 𝐴 “ 𝐵 ) )