Metamath Proof Explorer


Theorem mptresid

Description: The restricted identity relation expressed in maps-to notation. (Contributed by FL, 25-Apr-2012)

Ref Expression
Assertion mptresid I A = x A x

Proof

Step Hyp Ref Expression
1 opabresid I A = x y | x A y = x
2 df-mpt x A x = x y | x A y = x
3 1 2 eqtr4i I A = x A x