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 e. A |-> x )

Proof

Step Hyp Ref Expression
1 opabresid
 |-  ( _I |` A ) = { <. x , y >. | ( x e. A /\ y = x ) }
2 df-mpt
 |-  ( x e. A |-> x ) = { <. x , y >. | ( x e. A /\ y = x ) }
3 1 2 eqtr4i
 |-  ( _I |` A ) = ( x e. A |-> x )