Metamath Proof Explorer


Theorem resima

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

Ref Expression
Assertion resima ( ( 𝐴𝐵 ) “ 𝐵 ) = ( 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 residm ( ( 𝐴𝐵 ) ↾ 𝐵 ) = ( 𝐴𝐵 )
2 1 rneqi ran ( ( 𝐴𝐵 ) ↾ 𝐵 ) = ran ( 𝐴𝐵 )
3 df-ima ( ( 𝐴𝐵 ) “ 𝐵 ) = ran ( ( 𝐴𝐵 ) ↾ 𝐵 )
4 df-ima ( 𝐴𝐵 ) = ran ( 𝐴𝐵 )
5 2 3 4 3eqtr4i ( ( 𝐴𝐵 ) “ 𝐵 ) = ( 𝐴𝐵 )