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 IA×A=IA

Proof

Step Hyp Ref Expression
1 idinxpres IA×A=IAA
2 inidm AA=A
3 2 reseq2i IAA=IA
4 1 3 eqtri IA×A=IA