Description: A restriction of a Cartesian product is a Cartesian product. (Contributed by Stefan O'Rear, 24-Jan-2015) Extract from proof of xpssres . (Revised by BJ, 31-Oct-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | xpres | |- ( ( A X. B ) |` C ) = ( ( A i^i C ) X. B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-res | |- ( ( A X. B ) |` C ) = ( ( A X. B ) i^i ( C X. _V ) ) |
|
| 2 | inxp | |- ( ( A X. B ) i^i ( C X. _V ) ) = ( ( A i^i C ) X. ( B i^i _V ) ) |
|
| 3 | inv1 | |- ( B i^i _V ) = B |
|
| 4 | 3 | xpeq2i | |- ( ( A i^i C ) X. ( B i^i _V ) ) = ( ( A i^i C ) X. B ) |
| 5 | 1 2 4 | 3eqtri | |- ( ( A X. B ) |` C ) = ( ( A i^i C ) X. B ) |