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

Metamath Proof Explorer

Theorem idinxpresid

Description: The intersection of the identity relation with the cartesian square of a class is the restriction of the identity relation to that class. (Contributed by FL, 2-Aug-2009) (Proof shortened by Peter Mazsa, 9-Sep-2022) (Proof shortened by BJ, 23-Dec-2023)

Ref Expression
Assertion idinxpresid 
|- ( _I i^i ( A X. A ) ) = ( _I |` A )

Proof

Step Hyp Ref Expression
1 idinxpres 
 |-  ( _I i^i ( A X. A ) ) = ( _I |` ( A i^i A ) )
2 inidm 
 |-  ( A i^i A ) = A
3 2 reseq2i 
 |-  ( _I |` ( A i^i A ) ) = ( _I |` A )
4 1 3 eqtri 
 |-  ( _I i^i ( A X. A ) ) = ( _I |` A )