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 ⊢ B ⊆ C → A ↾ C B = A B

Proof

Step Hyp Ref Expression
1 sseqin2 ⊢ B ⊆ C ↔ C ∩ B = B
2 reseq2 ⊢ C ∩ B = B → A ↾ C ∩ B = A ↾ B
3 1 2 sylbi ⊢ B ⊆ C → A ↾ C ∩ B = A ↾ B
4 3 rneqd ⊢ B ⊆ C → ran ⁡ A ↾ C ∩ B = ran ⁡ A ↾ B
5 df-ima ⊢ A ↾ C B = ran ⁡ A ↾ C ↾ B
6 resres ⊢ A ↾ C ↾ B = A ↾ C ∩ B
7 6 rneqi ⊢ ran ⁡ A ↾ C ↾ B = ran ⁡ A ↾ C ∩ B
8 5 7 eqtri ⊢ A ↾ C B = ran ⁡ A ↾ C ∩ B
9 df-ima ⊢ A B = ran ⁡ A ↾ B
10 4 8 9 3eqtr4g ⊢ B ⊆ C → A ↾ C B = A B