Theorem opabresidOLD

Description: Obsolete version of opabresid as of 26-Dec-2023. (Contributed by FL, 25-Apr-2012) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	opabresidOLD	$$⊢\left\{⟨x,y⟩|\left(x\in A\wedge y=x\right)\right\}={\mathrm{I}\upharpoonright }_A$$

Proof

Step	Hyp	Ref	Expression
1		resopab	$$⊢{\left\{⟨x,y⟩|y=x\right\}\upharpoonright }_A=\left\{⟨x,y⟩|\left(x\in A\wedge y=x\right)\right\}$$
2		equcom	$$⊢y=x\leftrightarrow x=y$$
3	2	opabbii	$$⊢\left\{⟨x,y⟩|y=x\right\}=\left\{⟨x,y⟩|x=y\right\}$$
4		df-id	$$⊢\mathrm{I}=\left\{⟨x,y⟩|x=y\right\}$$
5	3 4	eqtr4i	$$⊢\left\{⟨x,y⟩|y=x\right\}=\mathrm{I}$$
6	5	reseq1i	$$⊢{\left\{⟨x,y⟩|y=x\right\}\upharpoonright }_A={\mathrm{I}\upharpoonright }_A$$
7	1 6	eqtr3i	$$⊢\left\{⟨x,y⟩|\left(x\in A\wedge y=x\right)\right\}={\mathrm{I}\upharpoonright }_A$$