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 )