This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iunin1f

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) (Revised by Thierry Arnoux, 2-May-2020)

		Ref	Expression
	Hypothesis	iunin1f.1	$⊢ \underline{Ⅎ} x C$
	Assertion	iunin1f	$⊢ ⋃_{x \in A} (B \cap C) = ⋃_{x \in A} B \cap C$

Proof

Step	Hyp	Ref	Expression
1		iunin1f.1	$⊢ \underline{Ⅎ} x C$
2	1	nfcri	$⊢ Ⅎ x y \in C$
3	2	r19.41	$⊢ \exists x \in A (y \in B \land y \in C) \leftrightarrow (\exists x \in A y \in B \land y \in C)$
4		elin	$⊢ y \in (B \cap C) \leftrightarrow (y \in B \land y \in C)$
5	4	rexbii	$⊢ \exists x \in A y \in (B \cap C) \leftrightarrow \exists x \in A (y \in B \land y \in C)$
6		eliun	$⊢ y \in ⋃_{x \in A} B \leftrightarrow \exists x \in A y \in B$
7	6	anbi1i	$⊢ (y \in ⋃_{x \in A} B \land y \in C) \leftrightarrow (\exists x \in A y \in B \land y \in C)$
8	3 5 7	3bitr4i	$⊢ \exists x \in A y \in (B \cap C) \leftrightarrow (y \in ⋃_{x \in A} B \land y \in C)$
9		eliun	$⊢ y \in ⋃_{x \in A} (B \cap C) \leftrightarrow \exists x \in A y \in (B \cap C)$
10		elin	$⊢ y \in (⋃_{x \in A} B \cap C) \leftrightarrow (y \in ⋃_{x \in A} B \land y \in C)$
11	8 9 10	3bitr4i	$⊢ y \in ⋃_{x \in A} (B \cap C) \leftrightarrow y \in (⋃_{x \in A} B \cap C)$
12	11	eqriv	$⊢ ⋃_{x \in A} (B \cap C) = ⋃_{x \in A} B \cap C$