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

Metamath Proof Explorer

Theorem imadmres

Description: The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007)

Ref Expression
Assertion imadmres ⊢ A dom ⁡ A ↾ B = A B

Proof

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