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

		Ref	Expression
	Assertion	inxp	$⊢ (A \times B) \cap (C \times D) = (A \cap C) \times (B \cap D)$

Proof

Step	Hyp	Ref	Expression
1		relinxp	$⊢ Rel ((A \times B) \cap (C \times D))$
2		relxp	$⊢ Rel ((A \cap C) \times (B \cap D))$
3		an4	$⊢ ((x \in A \land y \in B) \land (x \in C \land y \in D)) \leftrightarrow ((x \in A \land x \in C) \land (y \in B \land y \in D))$
4		opelxp	$⊢ ⟨x, y⟩ \in (A \times B) \leftrightarrow (x \in A \land y \in B)$
5		opelxp	$⊢ ⟨x, y⟩ \in (C \times D) \leftrightarrow (x \in C \land y \in D)$
6	4 5	anbi12i	$⊢ (⟨x, y⟩ \in (A \times B) \land ⟨x, y⟩ \in (C \times D)) \leftrightarrow ((x \in A \land y \in B) \land (x \in C \land y \in D))$
7		elin	$⊢ x \in (A \cap C) \leftrightarrow (x \in A \land x \in C)$
8		elin	$⊢ y \in (B \cap D) \leftrightarrow (y \in B \land y \in D)$
9	7 8	anbi12i	$⊢ (x \in (A \cap C) \land y \in (B \cap D)) \leftrightarrow ((x \in A \land x \in C) \land (y \in B \land y \in D))$
10	3 6 9	3bitr4i	$⊢ (⟨x, y⟩ \in (A \times B) \land ⟨x, y⟩ \in (C \times D)) \leftrightarrow (x \in (A \cap C) \land y \in (B \cap D))$
11		elin	$⊢ ⟨x, y⟩ \in ((A \times B) \cap (C \times D)) \leftrightarrow (⟨x, y⟩ \in (A \times B) \land ⟨x, y⟩ \in (C \times D))$
12		opelxp	$⊢ ⟨x, y⟩ \in ((A \cap C) \times (B \cap D)) \leftrightarrow (x \in (A \cap C) \land y \in (B \cap D))$
13	10 11 12	3bitr4i	$⊢ ⟨x, y⟩ \in ((A \times B) \cap (C \times D)) \leftrightarrow ⟨x, y⟩ \in ((A \cap C) \times (B \cap D))$
14	1 2 13	eqrelriiv	$⊢ (A \times B) \cap (C \times D) = (A \cap C) \times (B \cap D)$