Metamath Proof Explorer


Theorem mptresidOLD

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 A x = I A

Proof

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