Theorem idreseqidinxp

Description: Condition for the identity restriction to be equal to the identity intersection with a Cartesian product. (Contributed by Peter Mazsa, 19-Jul-2018)

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

Proof

Step	Hyp	Ref	Expression
1		inxpssres	$$⊢\mathrm{I}\cap \left(A\times B\right)\subseteq {\mathrm{I}\upharpoonright }_A$$
2	1	a1i	$$⊢A\subseteq B\to \mathrm{I}\cap \left(A\times B\right)\subseteq {\mathrm{I}\upharpoonright }_A$$
3		idresssidinxp	$$⊢A\subseteq B\to {\mathrm{I}\upharpoonright }_A\subseteq \mathrm{I}\cap \left(A\times B\right)$$
4	2 3	eqssd	$$⊢A\subseteq B\to \mathrm{I}\cap \left(A\times B\right)={\mathrm{I}\upharpoonright }_A$$