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 ↾ 𝐴 ) ⊆ ( 𝐴 × 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		idinxpresid	⊢ ( I ∩ ( 𝐴 × 𝐴 ) ) = ( I ↾ 𝐴 )
2		inss2	⊢ ( I ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 )
3	1 2	eqsstrri	⊢ ( I ↾ 𝐴 ) ⊆ ( 𝐴 × 𝐴 )