Theorem idinxpres

Description: The intersection of the identity relation with a cartesian product is the restriction of the identity relation to the intersection of the factors. (Contributed by FL, 2-Aug-2009) (Proof shortened by Peter Mazsa, 9-Sep-2022) Generalize statement from cartesian square (now idinxpresid ) to cartesian product. (Revised by BJ, 23-Dec-2023)

	Ref	Expression
Assertion	idinxpres	$$⊢\mathrm{I}\cap \left(A\times B\right)={\mathrm{I}\upharpoonright }_{\left(A\cap B\right)}$$

Proof

Step	Hyp	Ref	Expression
1		elidinxp	$$⊢x\in \left(\mathrm{I}\cap \left(A\times B\right)\right)\leftrightarrow \exists y\in \left(A\cap B\right)x=⟨y,y⟩$$
2		elrid	$$⊢x\in \left({\mathrm{I}\upharpoonright }_{\left(A\cap B\right)}\right)\leftrightarrow \exists y\in \left(A\cap B\right)x=⟨y,y⟩$$
3	1 2	bitr4i	$$⊢x\in \left(\mathrm{I}\cap \left(A\times B\right)\right)\leftrightarrow x\in \left({\mathrm{I}\upharpoonright }_{\left(A\cap B\right)}\right)$$
4	3	eqriv	$$⊢\mathrm{I}\cap \left(A\times B\right)={\mathrm{I}\upharpoonright }_{\left(A\cap B\right)}$$