Theorem idinxpresid

Description: The intersection of the identity relation with the cartesian square of a class is the restriction of the identity relation to that class. (Contributed by FL, 2-Aug-2009) (Proof shortened by Peter Mazsa, 9-Sep-2022) (Proof shortened by BJ, 23-Dec-2023)

	Ref	Expression
Assertion	idinxpresid	$$⊢\mathrm{I}\cap \left(A\times A\right)={\mathrm{I}\upharpoonright }_A$$

Proof

Step	Hyp	Ref	Expression
1		idinxpres	$$⊢\mathrm{I}\cap \left(A\times A\right)={\mathrm{I}\upharpoonright }_{\left(A\cap A\right)}$$
2		inidm	$$⊢A\cap A=A$$
3	2	reseq2i	$$⊢{\mathrm{I}\upharpoonright }_{\left(A\cap A\right)}={\mathrm{I}\upharpoonright }_A$$
4	1 3	eqtri	$$⊢\mathrm{I}\cap \left(A\times A\right)={\mathrm{I}\upharpoonright }_A$$