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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idinxpres | |
|
2 | inidm | |
|
3 | 2 | reseq2i | |
4 | 1 3 | eqtri | |