Metamath Proof Explorer

Theorem undi

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

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

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ x \in (B \cap C) \leftrightarrow (x \in B \land x \in C)$
2	1	orbi2i	$⊢ (x \in A \lor x \in (B \cap C)) \leftrightarrow (x \in A \lor (x \in B \land x \in C))$
3		ordi	$⊢ (x \in A \lor (x \in B \land x \in C)) \leftrightarrow ((x \in A \lor x \in B) \land (x \in A \lor x \in C))$
4		elin	$⊢ x \in ((A \cup B) \cap (A \cup C)) \leftrightarrow (x \in (A \cup B) \land x \in (A \cup C))$
5		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
6		elun	$⊢ x \in (A \cup C) \leftrightarrow (x \in A \lor x \in C)$
7	5 6	anbi12i	$⊢ (x \in (A \cup B) \land x \in (A \cup C)) \leftrightarrow ((x \in A \lor x \in B) \land (x \in A \lor x \in C))$
8	4 7	bitr2i	$⊢ ((x \in A \lor x \in B) \land (x \in A \lor x \in C)) \leftrightarrow x \in ((A \cup B) \cap (A \cup C))$
9	2 3 8	3bitri	$⊢ (x \in A \lor x \in (B \cap C)) \leftrightarrow x \in ((A \cup B) \cap (A \cup C))$
10	9	uneqri	$⊢ A \cup (B \cap C) = (A \cup B) \cap (A \cup C)$