intun

Description: The class intersection of the union of two classes. Theorem 78 of Suppes p. 42. (Contributed by NM, 22-Sep-2002)

		Ref	Expression
	Assertion	intun	$⊢ ⋂ (A \cup B) = ⋂ A \cap ⋂ B$

Step	Hyp	Ref	Expression
1		19.26	$⊢ \forall y ((y \in A \to x \in y) \land (y \in B \to x \in y)) \leftrightarrow (\forall y (y \in A \to x \in y) \land \forall y (y \in B \to x \in y))$
2		elunant	$⊢ (y \in (A \cup B) \to x \in y) \leftrightarrow ((y \in A \to x \in y) \land (y \in B \to x \in y))$
3	2	albii	$⊢ \forall y (y \in (A \cup B) \to x \in y) \leftrightarrow \forall y ((y \in A \to x \in y) \land (y \in B \to x \in y))$
4		vex	$⊢ x \in V$
5	4	elint	$⊢ x \in ⋂ A \leftrightarrow \forall y (y \in A \to x \in y)$
6	4	elint	$⊢ x \in ⋂ B \leftrightarrow \forall y (y \in B \to x \in y)$
7	5 6	anbi12i	$⊢ (x \in ⋂ A \land x \in ⋂ B) \leftrightarrow (\forall y (y \in A \to x \in y) \land \forall y (y \in B \to x \in y))$
8	1 3 7	3bitr4i	$⊢ \forall y (y \in (A \cup B) \to x \in y) \leftrightarrow (x \in ⋂ A \land x \in ⋂ B)$
9	4	elint	$⊢ x \in ⋂ (A \cup B) \leftrightarrow \forall y (y \in (A \cup B) \to x \in y)$
10		elin	$⊢ x \in (⋂ A \cap ⋂ B) \leftrightarrow (x \in ⋂ A \land x \in ⋂ B)$
11	8 9 10	3bitr4i	$⊢ x \in ⋂ (A \cup B) \leftrightarrow x \in (⋂ A \cap ⋂ B)$
12	11	eqriv	$⊢ ⋂ (A \cup B) = ⋂ A \cap ⋂ B$

Metamath Proof Explorer