Description: The intersection of the identity relation with a cartesian product is
the restriction of the identity relation to the intersection of the
factors. (Contributed by FL, 2-Aug-2009)(Proof shortened by Peter
Mazsa, 9-Sep-2022) Generalize statement from cartesian square (now
idinxpresid ) to cartesian product. (Revised by BJ, 23-Dec-2023)