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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | idinxpres | |- ( _I i^i ( A X. B ) ) = ( _I |` ( A i^i B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elidinxp | |- ( x e. ( _I i^i ( A X. B ) ) <-> E. y e. ( A i^i B ) x = <. y , y >. ) |
|
| 2 | elrid | |- ( x e. ( _I |` ( A i^i B ) ) <-> E. y e. ( A i^i B ) x = <. y , y >. ) |
|
| 3 | 1 2 | bitr4i | |- ( x e. ( _I i^i ( A X. B ) ) <-> x e. ( _I |` ( A i^i B ) ) ) |
| 4 | 3 | eqriv | |- ( _I i^i ( A X. B ) ) = ( _I |` ( A i^i B ) ) |