This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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