Description: Obsolete version of mptresid as of 26-Dec-2023. (Contributed by FL, 25-Apr-2012) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | mptresidOLD | |- ( x e. A |-> x ) = ( _I |` A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-mpt | |- ( x e. A |-> x ) = { <. x , y >. | ( x e. A /\ y = x ) } |
|
| 2 | opabresidOLD | |- { <. x , y >. | ( x e. A /\ y = x ) } = ( _I |` A ) |
|
| 3 | 1 2 | eqtri | |- ( x e. A |-> x ) = ( _I |` A ) |