Theorem inxp 5815

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 2180, ax-12 2216. (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 5797	. 2 ⊢ Rel ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷))
2		relxp 5673	. 2 ⊢ Rel ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷))
3		an4 669	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
4		opelxp 5691	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5		opelxp 5691	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐶 × 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷))
6	4, 5	anbi12i 640	. . . 4 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐶 × 𝐷)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
7		elin 4096	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
8		elin 4096	. . . . 5 ⊢ (𝑦 ∈ (𝐵 ∩ 𝐷) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷))
9	7, 8	anbi12i 640	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐶) ∧ 𝑦 ∈ (𝐵 ∩ 𝐷)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
10	3, 6, 9	3bitr4i 306	. . 3 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐶 × 𝐷)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ 𝑦 ∈ (𝐵 ∩ 𝐷)))
11		elin 4096	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐶 × 𝐷)))
12		opelxp 5691	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷)) ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ 𝑦 ∈ (𝐵 ∩ 𝐷)))
13	10, 11, 12	3bitr4i 306	. 2 ⊢ (⟨𝑥, 𝑦⟩ ∈ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷)))
14	1, 2, 13	eqrelriiv 5771	1 ⊢ ((𝐴 × 𝐵) ∩ (𝐶 × 𝐷)) = ((𝐴 ∩ 𝐶) × (𝐵 ∩ 𝐷))

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ∩ cin 4092  ⟨cop 4838   × cxp 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-opab 5171  df-xp 5661  df-rel 5662

This theorem is used by:  xpindi  5816  xpindir  5817  dmxpin  5920  xpssres  6019  xpdisj1  6164  xpdisj2  6165  imainrect  6185  xpima  6186  cnvrescnv  6200  curry1  8142  curry2  8145  fpar  8154  marypha1lem  9452  fpwwe2lem12  10754  hashxplem  14605  sscres  18027  gsumxp  20220  pjfval  22042  pjpm  22044  txbas  23916  txcls  23953  txrest  23980  trust  24578  ressuss  24611  trcfilu  24642  metreslem  24711  ressxms  24874  ressms  24875  mbfmcst  34961  0rrv  35153  poimirlem26  38756