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)