Theorem idssxp

Description: A diagonal set as a subset of a Cartesian square. (Contributed by Thierry Arnoux, 29-Dec-2019) (Proof shortened by BJ, 9-Sep-2022)

	Ref	Expression
Assertion	idssxp	$$⊢{\mathrm{I}\upharpoonright }_A\subseteq A\times A$$

Proof

Step	Hyp	Ref	Expression
1		idinxpresid	$$⊢\mathrm{I}\cap \left(A\times A\right)={\mathrm{I}\upharpoonright }_A$$
2		inss2	$$⊢\mathrm{I}\cap \left(A\times A\right)\subseteq A\times A$$
3	1 2	eqsstrri	$$⊢{\mathrm{I}\upharpoonright }_A\subseteq A\times A$$