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 ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) = ( ( 𝐴𝐶 ) × ( 𝐵𝐷 ) )

Proof

Step Hyp Ref Expression
1 inopab ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦𝐵 ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝑦𝐷 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑥𝐶𝑦𝐷 ) ) }
2 an4 ( ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑥𝐶𝑦𝐷 ) ) ↔ ( ( 𝑥𝐴𝑥𝐶 ) ∧ ( 𝑦𝐵𝑦𝐷 ) ) )
3 elin ( 𝑥 ∈ ( 𝐴𝐶 ) ↔ ( 𝑥𝐴𝑥𝐶 ) )
4 elin ( 𝑦 ∈ ( 𝐵𝐷 ) ↔ ( 𝑦𝐵𝑦𝐷 ) )
5 3 4 anbi12i ( ( 𝑥 ∈ ( 𝐴𝐶 ) ∧ 𝑦 ∈ ( 𝐵𝐷 ) ) ↔ ( ( 𝑥𝐴𝑥𝐶 ) ∧ ( 𝑦𝐵𝑦𝐷 ) ) )
6 2 5 bitr4i ( ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑥𝐶𝑦𝐷 ) ) ↔ ( 𝑥 ∈ ( 𝐴𝐶 ) ∧ 𝑦 ∈ ( 𝐵𝐷 ) ) )
7 6 opabbii { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑥𝐶𝑦𝐷 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴𝐶 ) ∧ 𝑦 ∈ ( 𝐵𝐷 ) ) }
8 1 7 eqtri ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦𝐵 ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝑦𝐷 ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴𝐶 ) ∧ 𝑦 ∈ ( 𝐵𝐷 ) ) }
9 df-xp ( 𝐴 × 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦𝐵 ) }
10 df-xp ( 𝐶 × 𝐷 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝑦𝐷 ) }
11 9 10 ineq12i ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦𝐵 ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝑦𝐷 ) } )
12 df-xp ( ( 𝐴𝐶 ) × ( 𝐵𝐷 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴𝐶 ) ∧ 𝑦 ∈ ( 𝐵𝐷 ) ) }
13 8 11 12 3eqtr4i ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) = ( ( 𝐴𝐶 ) × ( 𝐵𝐷 ) )