# Metamath Proof Explorer

## Theorem inxp

Description: Intersection of two Cartesian products. Exercise 9 of TakeutiZaring p. 25. (Contributed by NM, 3-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion inxp ${⊢}\left({A}×{B}\right)\cap \left({C}×{D}\right)=\left({A}\cap {C}\right)×\left({B}\cap {D}\right)$

### Proof

Step Hyp Ref Expression
1 inopab ${⊢}\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {B}\right)\right\}\cap \left\{⟨{x},{y}⟩|\left({x}\in {C}\wedge {y}\in {D}\right)\right\}=\left\{⟨{x},{y}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({x}\in {C}\wedge {y}\in {D}\right)\right)\right\}$
2 an4 ${⊢}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({x}\in {C}\wedge {y}\in {D}\right)\right)↔\left(\left({x}\in {A}\wedge {x}\in {C}\right)\wedge \left({y}\in {B}\wedge {y}\in {D}\right)\right)$
3 elin ${⊢}{x}\in \left({A}\cap {C}\right)↔\left({x}\in {A}\wedge {x}\in {C}\right)$
4 elin ${⊢}{y}\in \left({B}\cap {D}\right)↔\left({y}\in {B}\wedge {y}\in {D}\right)$
5 3 4 anbi12i ${⊢}\left({x}\in \left({A}\cap {C}\right)\wedge {y}\in \left({B}\cap {D}\right)\right)↔\left(\left({x}\in {A}\wedge {x}\in {C}\right)\wedge \left({y}\in {B}\wedge {y}\in {D}\right)\right)$
6 2 5 bitr4i ${⊢}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({x}\in {C}\wedge {y}\in {D}\right)\right)↔\left({x}\in \left({A}\cap {C}\right)\wedge {y}\in \left({B}\cap {D}\right)\right)$
7 6 opabbii ${⊢}\left\{⟨{x},{y}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({x}\in {C}\wedge {y}\in {D}\right)\right)\right\}=\left\{⟨{x},{y}⟩|\left({x}\in \left({A}\cap {C}\right)\wedge {y}\in \left({B}\cap {D}\right)\right)\right\}$
8 1 7 eqtri ${⊢}\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {B}\right)\right\}\cap \left\{⟨{x},{y}⟩|\left({x}\in {C}\wedge {y}\in {D}\right)\right\}=\left\{⟨{x},{y}⟩|\left({x}\in \left({A}\cap {C}\right)\wedge {y}\in \left({B}\cap {D}\right)\right)\right\}$
9 df-xp ${⊢}{A}×{B}=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {B}\right)\right\}$
10 df-xp ${⊢}{C}×{D}=\left\{⟨{x},{y}⟩|\left({x}\in {C}\wedge {y}\in {D}\right)\right\}$
11 9 10 ineq12i ${⊢}\left({A}×{B}\right)\cap \left({C}×{D}\right)=\left\{⟨{x},{y}⟩|\left({x}\in {A}\wedge {y}\in {B}\right)\right\}\cap \left\{⟨{x},{y}⟩|\left({x}\in {C}\wedge {y}\in {D}\right)\right\}$
12 df-xp ${⊢}\left({A}\cap {C}\right)×\left({B}\cap {D}\right)=\left\{⟨{x},{y}⟩|\left({x}\in \left({A}\cap {C}\right)\wedge {y}\in \left({B}\cap {D}\right)\right)\right\}$
13 8 11 12 3eqtr4i ${⊢}\left({A}×{B}\right)\cap \left({C}×{D}\right)=\left({A}\cap {C}\right)×\left({B}\cap {D}\right)$