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	$⊢ (A \times B) \cap (C \times D) = (A \cap C) \times (B \cap D)$

Proof

Step	Hyp	Ref	Expression
1		inopab	$⊢ \{⟨x, y⟩ \| (x \in A \land y \in B)\} \cap \{⟨x, y⟩ \| (x \in C \land y \in D)\} = \{⟨x, y⟩ \| ((x \in A \land y \in B) \land (x \in C \land y \in D))\}$
2		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))$
3		elin	$⊢ x \in (A \cap C) \leftrightarrow (x \in A \land x \in C)$
4		elin	$⊢ y \in (B \cap D) \leftrightarrow (y \in B \land y \in D)$
5	3 4	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))$
6	2 5	bitr4i	$⊢ ((x \in A \land y \in B) \land (x \in C \land y \in D)) \leftrightarrow (x \in (A \cap C) \land y \in (B \cap D))$
7	6	opabbii	$⊢ \{⟨x, y⟩ \| ((x \in A \land y \in B) \land (x \in C \land y \in D))\} = \{⟨x, y⟩ \| (x \in (A \cap C) \land y \in (B \cap D))\}$
8	1 7	eqtri	$⊢ \{⟨x, y⟩ \| (x \in A \land y \in B)\} \cap \{⟨x, y⟩ \| (x \in C \land y \in D)\} = \{⟨x, y⟩ \| (x \in (A \cap C) \land y \in (B \cap D))\}$
9		df-xp	$⊢ A \times B = \{⟨x, y⟩ \| (x \in A \land y \in B)\}$
10		df-xp	$⊢ C \times D = \{⟨x, y⟩ \| (x \in C \land y \in D)\}$
11	9 10	ineq12i	$⊢ (A \times B) \cap (C \times D) = \{⟨x, y⟩ \| (x \in A \land y \in B)\} \cap \{⟨x, y⟩ \| (x \in C \land y \in D)\}$
12		df-xp	$⊢ (A \cap C) \times (B \cap D) = \{⟨x, y⟩ \| (x \in (A \cap C) \land y \in (B \cap D))\}$
13	8 11 12	3eqtr4i	$⊢ (A \times B) \cap (C \times D) = (A \cap C) \times (B \cap D)$