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) (Proof shortened by Wolf Lammen, 15-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		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)$
2		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)$
3	1 2	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)$
4	3	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)$
5		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)$
6		eluni2	$⊢ z \in ⋃ A \leftrightarrow \exists y \in A z \in y$
7	6	anbi1i	$⊢ (z \in ⋃ A \land z \in B) \leftrightarrow (\exists y \in A z \in y \land z \in B)$
8		elin	$⊢ z \in (⋃ A \cap B) \leftrightarrow (z \in ⋃ A \land z \in B)$
9		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)$
10	7 8 9	3bitr4i	$⊢ z \in (⋃ A \cap B) \leftrightarrow \exists y \in A (z \in y \land z \in B)$
11		vex	$⊢ y \in V$
12	11	inex1	$⊢ y \cap B \in V$
13		eleq2	$⊢ x = y \cap B \to (z \in x \leftrightarrow z \in (y \cap B))$
14	12 13	ceqsexv	$⊢ \exists x (x = y \cap B \land z \in x) \leftrightarrow z \in (y \cap B)$
15		elin	$⊢ z \in (y \cap B) \leftrightarrow (z \in y \land z \in B)$
16	14 15	bitri	$⊢ \exists x (x = y \cap B \land z \in x) \leftrightarrow (z \in y \land z \in B)$
17	16	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)$
18		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)$
19	10 17 18	3bitr2i	$⊢ z \in (⋃ A \cap B) \leftrightarrow \exists x \exists y \in A (x = y \cap B \land z \in x)$
20	4 5 19	3bitr4ri	$⊢ z \in (⋃ A \cap B) \leftrightarrow z \in ⋃ \{x \| \exists y \in A x = y \cap B\}$
21	20	eqriv	$⊢ ⋃ A \cap B = ⋃ \{x \| \exists y \in A x = y \cap B\}$

Metamath Proof Explorer

Theorem inuni

Proof