Metamath Proof Explorer

Theorem uniin

Description: The class union of the intersection of two classes. Exercise 4.12(n) of Mendelson p. 235. See uniinqs for a condition where equality holds. (Contributed by NM, 4-Dec-2003) (Proof shortened by Andrew Salmon, 29-Jun-2011)

		Ref	Expression
	Assertion	uniin	$⊢ ⋃ (A \cap B) \subseteq ⋃ A \cap ⋃ B$

Proof

Step	Hyp	Ref	Expression
1		19.40	$⊢ \exists y ((x \in y \land y \in A) \land (x \in y \land y \in B)) \to (\exists y (x \in y \land y \in A) \land \exists y (x \in y \land y \in B))$
2		elin	$⊢ y \in (A \cap B) \leftrightarrow (y \in A \land y \in B)$
3	2	anbi2i	$⊢ (x \in y \land y \in (A \cap B)) \leftrightarrow (x \in y \land (y \in A \land y \in B))$
4		anandi	$⊢ (x \in y \land (y \in A \land y \in B)) \leftrightarrow ((x \in y \land y \in A) \land (x \in y \land y \in B))$
5	3 4	bitri	$⊢ (x \in y \land y \in (A \cap B)) \leftrightarrow ((x \in y \land y \in A) \land (x \in y \land y \in B))$
6	5	exbii	$⊢ \exists y (x \in y \land y \in (A \cap B)) \leftrightarrow \exists y ((x \in y \land y \in A) \land (x \in y \land y \in B))$
7		eluni	$⊢ x \in ⋃ A \leftrightarrow \exists y (x \in y \land y \in A)$
8		eluni	$⊢ x \in ⋃ B \leftrightarrow \exists y (x \in y \land y \in B)$
9	7 8	anbi12i	$⊢ (x \in ⋃ A \land x \in ⋃ B) \leftrightarrow (\exists y (x \in y \land y \in A) \land \exists y (x \in y \land y \in B))$
10	1 6 9	3imtr4i	$⊢ \exists y (x \in y \land y \in (A \cap B)) \to (x \in ⋃ A \land x \in ⋃ B)$
11		eluni	$⊢ x \in ⋃ (A \cap B) \leftrightarrow \exists y (x \in y \land y \in (A \cap B))$
12		elin	$⊢ x \in (⋃ A \cap ⋃ B) \leftrightarrow (x \in ⋃ A \land x \in ⋃ B)$
13	10 11 12	3imtr4i	$⊢ x \in ⋃ (A \cap B) \to x \in (⋃ A \cap ⋃ B)$
14	13	ssriv	$⊢ ⋃ (A \cap B) \subseteq ⋃ A \cap ⋃ B$