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 ) C_ ( A X. A )

Proof

Step Hyp Ref Expression
1 idinxpresid 
 |-  ( _I i^i ( A X. A ) ) = ( _I |` A )
2 inss2 
 |-  ( _I i^i ( A X. A ) ) C_ ( A X. A )
3 1 2 eqsstrri 
 |-  ( _I |` A ) C_ ( A X. A )