This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inxpOLD

Description: Obsolete version of inxp as of 5-May-2025. (Contributed by NM, 3-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion inxpOLD ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × 𝐷 ) ) = ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ 𝐷 ) )

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