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

Metamath Proof Explorer

Theorem resima

Description: A restriction to an image. (Contributed by NM, 29-Sep-2004)

Ref Expression
Assertion resima ⊢ A ↾ B B = A B

Proof

Step Hyp Ref Expression
1 residm ⊢ A ↾ B ↾ B = A ↾ B
2 1 rneqi ⊢ ran ⁡ A ↾ B ↾ B = ran ⁡ A ↾ B
3 df-ima ⊢ A ↾ B B = ran ⁡ A ↾ B ↾ B
4 df-ima ⊢ A B = ran ⁡ A ↾ B
5 2 3 4 3eqtr4i ⊢ A ↾ B B = A B