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 | ⊢ ( ( 𝐴 × 𝐵 ) ↾ 𝐶 ) = ( ( 𝐴 ∩ 𝐶 ) × 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-res | ⊢ ( ( 𝐴 × 𝐵 ) ↾ 𝐶 ) = ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × V ) ) | |
| 2 | inxp | ⊢ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × V ) ) = ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ V ) ) | |
| 3 | inv1 | ⊢ ( 𝐵 ∩ V ) = 𝐵 | |
| 4 | 3 | xpeq2i | ⊢ ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ V ) ) = ( ( 𝐴 ∩ 𝐶 ) × 𝐵 ) |
| 5 | 1 2 4 | 3eqtri | ⊢ ( ( 𝐴 × 𝐵 ) ↾ 𝐶 ) = ( ( 𝐴 ∩ 𝐶 ) × 𝐵 ) |