Metamath Proof Explorer

Theorem iunin2

Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in Enderton p. 30. Use uniiun to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004)

		Ref	Expression
	Assertion	iunin2	$⊢ ⋃_{x \in A} (B \cap C) = B \cap ⋃_{x \in A} C$

Proof

Step	Hyp	Ref	Expression
1		r19.42v	$⊢ \exists x \in A (y \in B \land y \in C) \leftrightarrow (y \in B \land \exists x \in A y \in C)$
2		elin	$⊢ y \in (B \cap C) \leftrightarrow (y \in B \land y \in C)$
3	2	rexbii	$⊢ \exists x \in A y \in (B \cap C) \leftrightarrow \exists x \in A (y \in B \land y \in C)$
4		eliun	$⊢ y \in ⋃_{x \in A} C \leftrightarrow \exists x \in A y \in C$
5	4	anbi2i	$⊢ (y \in B \land y \in ⋃_{x \in A} C) \leftrightarrow (y \in B \land \exists x \in A y \in C)$
6	1 3 5	3bitr4i	$⊢ \exists x \in A y \in (B \cap C) \leftrightarrow (y \in B \land y \in ⋃_{x \in A} C)$
7		eliun	$⊢ y \in ⋃_{x \in A} (B \cap C) \leftrightarrow \exists x \in A y \in (B \cap C)$
8		elin	$⊢ y \in (B \cap ⋃_{x \in A} C) \leftrightarrow (y \in B \land y \in ⋃_{x \in A} C)$
9	6 7 8	3bitr4i	$⊢ y \in ⋃_{x \in A} (B \cap C) \leftrightarrow y \in (B \cap ⋃_{x \in A} C)$
10	9	eqriv	$⊢ ⋃_{x \in A} (B \cap C) = B \cap ⋃_{x \in A} C$