Metamath Proof Explorer


Theorem resima

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

Ref Expression
Assertion resima ABB=AB

Proof

Step Hyp Ref Expression
1 residm ABB=AB
2 1 rneqi ranABB=ranAB
3 df-ima ABB=ranABB
4 df-ima AB=ranAB
5 2 3 4 3eqtr4i ABB=AB