Theorem opabresid

Description: The restricted identity relation expressed as an ordered-pair class abstraction. (Contributed by FL, 25-Apr-2012)

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

Proof

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