Theorem inxp 5802

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.) Avoid ax-10 2174, ax-12 2211. (Revised by SN, 5-May-2025.)

Assertion

Ref	Expression
inxp	⊢ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷))

Proof of Theorem inxp

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relinxp 5785	. 2 ⊢ Rel ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷))
2		relxp 5663	. 2 ⊢ Rel ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷))
3		an4 666	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
4		opelxp 5681	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5		opelxp 5681	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐶 × 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷))
6	4, 5	anbi12i 637	. . . 4 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐶 × 𝐷)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
7		elin 3920	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
8		elin 3920	. . . . 5 ⊢ (𝑦 ∈ (𝐵 ∩ 𝐷) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷))
9	7, 8	anbi12i 637	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐶) ∧ 𝑦 ∈ (𝐵 ∩ 𝐷)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
10	3, 6, 9	3bitr4i 305	. . 3 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐶 × 𝐷)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ 𝑦 ∈ (𝐵 ∩ 𝐷)))
11		elin 3920	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐶 × 𝐷)))
12		opelxp 5681	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ 𝑦 ∈ (𝐵 ∩ 𝐷)))
13	10, 11, 12	3bitr4i 305	. 2 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷)))
14	1, 2, 13	eqrelriiv 5760	1 ⊢ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷))

Syntax hints:   ∧ wa 399   = wceq 1559   ∈ wcel 2141   ∩ cin 3903  ⟨cop 4587   × cxp 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-opab 5162  df-xp 5651  df-rel 5652

This theorem is referenced by:  xpindi  5803  xpindir  5804  dmxpin  5905  xpssres  6002  xpdisj1  6143  xpdisj2  6144  imainrect  6163  xpima  6164  cnvrescnv  6178  curry1  8078  curry2  8081  fpar  8090  marypha1lem  9376  fpwwe2lem12  10597  hashxplem  14443  sscres  17839  gsumxp  19999  pjfval  21738  pjpm  21740  txbas  23607  txcls  23644  txrest  23671  trust  24269  ressuss  24302  trcfilu  24333  metreslem  24402  ressxms  24565  ressms  24566  mbfmcst  34517  0rrv  34709  poimirlem26  38109