inuni

Description: The intersection of a union U. A with a class B is equal to the union of the intersections of each element of A with B . (Contributed by FL, 24-Mar-2007)

		Ref	Expression
	Assertion	inuni	$⊢ ⋃ A \cap B = ⋃ \{x \| \exists y \in A x = y \cap B\}$

Proof

Step	Hyp	Ref	Expression
1		eluni2	$⊢ z \in ⋃ A \leftrightarrow \exists y \in A z \in y$
2	1	anbi1i	$⊢ (z \in ⋃ A \land z \in B) \leftrightarrow (\exists y \in A z \in y \land z \in B)$
3		elin	$⊢ z \in (⋃ A \cap B) \leftrightarrow (z \in ⋃ A \land z \in B)$
4		ancom	$⊢ (z \in x \land \exists y \in A x = y \cap B) \leftrightarrow (\exists y \in A x = y \cap B \land z \in x)$
5		r19.41v	$⊢ \exists y \in A (x = y \cap B \land z \in x) \leftrightarrow (\exists y \in A x = y \cap B \land z \in x)$
6	4 5	bitr4i	$⊢ (z \in x \land \exists y \in A x = y \cap B) \leftrightarrow \exists y \in A (x = y \cap B \land z \in x)$
7	6	exbii	$⊢ \exists x (z \in x \land \exists y \in A x = y \cap B) \leftrightarrow \exists x \exists y \in A (x = y \cap B \land z \in x)$
8		rexcom4	$⊢ \exists y \in A \exists x (x = y \cap B \land z \in x) \leftrightarrow \exists x \exists y \in A (x = y \cap B \land z \in x)$
9	7 8	bitr4i	$⊢ \exists x (z \in x \land \exists y \in A x = y \cap B) \leftrightarrow \exists y \in A \exists x (x = y \cap B \land z \in x)$
10		vex	$⊢ y \in V$
11	10	inex1	$⊢ y \cap B \in V$
12		eleq2	$⊢ x = y \cap B \to (z \in x \leftrightarrow z \in (y \cap B))$
13	11 12	ceqsexv	$⊢ \exists x (x = y \cap B \land z \in x) \leftrightarrow z \in (y \cap B)$
14		elin	$⊢ z \in (y \cap B) \leftrightarrow (z \in y \land z \in B)$
15	13 14	bitri	$⊢ \exists x (x = y \cap B \land z \in x) \leftrightarrow (z \in y \land z \in B)$
16	15	rexbii	$⊢ \exists y \in A \exists x (x = y \cap B \land z \in x) \leftrightarrow \exists y \in A (z \in y \land z \in B)$
17		r19.41v	$⊢ \exists y \in A (z \in y \land z \in B) \leftrightarrow (\exists y \in A z \in y \land z \in B)$
18	16 17	bitri	$⊢ \exists y \in A \exists x (x = y \cap B \land z \in x) \leftrightarrow (\exists y \in A z \in y \land z \in B)$
19	9 18	bitri	$⊢ \exists x (z \in x \land \exists y \in A x = y \cap B) \leftrightarrow (\exists y \in A z \in y \land z \in B)$
20	2 3 19	3bitr4i	$⊢ z \in (⋃ A \cap B) \leftrightarrow \exists x (z \in x \land \exists y \in A x = y \cap B)$
21		eluniab	$⊢ z \in ⋃ \{x \| \exists y \in A x = y \cap B\} \leftrightarrow \exists x (z \in x \land \exists y \in A x = y \cap B)$
22	20 21	bitr4i	$⊢ z \in (⋃ A \cap B) \leftrightarrow z \in ⋃ \{x \| \exists y \in A x = y \cap B\}$
23	22	eqriv	$⊢ ⋃ A \cap B = ⋃ \{x \| \exists y \in A x = y \cap B\}$

Metamath Proof Explorer

Theorem inuni

Proof