This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ {I ↾}_{A} \subseteq A \times A$

Step	Hyp	Ref	Expression
1		idinxpresid	$⊢ I \cap (A \times A) = {I ↾}_{A}$
2		inss2	$⊢ I \cap (A \times A) \subseteq A \times A$
3	1 2	eqsstrri	$⊢ {I ↾}_{A} \subseteq A \times A$