Metamath Proof Explorer

Theorem indi

Description: Distributive law for intersection over union. Exercise 10 of TakeutiZaring p. 17. (Contributed by NM, 30-Sep-2002) (Proof shortened by Andrew Salmon, 26-Jun-2011)

		Ref	Expression
	Assertion	indi	$⊢ A \cap (B \cup C) = (A \cap B) \cup (A \cap C)$

Proof

Step	Hyp	Ref	Expression
1		andi	$⊢ (x \in A \land (x \in B \lor x \in C)) \leftrightarrow ((x \in A \land x \in B) \lor (x \in A \land x \in C))$
2		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
3		elin	$⊢ x \in (A \cap C) \leftrightarrow (x \in A \land x \in C)$
4	2 3	orbi12i	$⊢ (x \in (A \cap B) \lor x \in (A \cap C)) \leftrightarrow ((x \in A \land x \in B) \lor (x \in A \land x \in C))$
5	1 4	bitr4i	$⊢ (x \in A \land (x \in B \lor x \in C)) \leftrightarrow (x \in (A \cap B) \lor x \in (A \cap C))$
6		elun	$⊢ x \in (B \cup C) \leftrightarrow (x \in B \lor x \in C)$
7	6	anbi2i	$⊢ (x \in A \land x \in (B \cup C)) \leftrightarrow (x \in A \land (x \in B \lor x \in C))$
8		elun	$⊢ x \in ((A \cap B) \cup (A \cap C)) \leftrightarrow (x \in (A \cap B) \lor x \in (A \cap C))$
9	5 7 8	3bitr4i	$⊢ (x \in A \land x \in (B \cup C)) \leftrightarrow x \in ((A \cap B) \cup (A \cap C))$
10	9	ineqri	$⊢ A \cap (B \cup C) = (A \cap B) \cup (A \cap C)$