Theorem inuni 5330

Description: The intersection of a union ∪ 𝐴 with a class 𝐵 is equal to the union of the intersections of each element of 𝐴 with 𝐵. (Contributed by FL, 24-Mar-2007.) (Proof shortened by Wolf Lammen, 15-May-2025.)

Assertion

Ref	Expression
inuni	⊢ (∪ 𝐴 ∩ 𝐵) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)}

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Proof of Theorem inuni

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ancom 460	. . . . 5 ⊢ ((𝑧 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)) ↔ (∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥))
2		r19.41v 3176	. . . . 5 ⊢ (∃𝑦 ∈ 𝐴 (𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥) ↔ (∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥))
3	1, 2	bitr4i 278	. . . 4 ⊢ ((𝑧 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)) ↔ ∃𝑦 ∈ 𝐴 (𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥))
4	3	exbii 1847	. . 3 ⊢ (∃𝑥(𝑧 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)) ↔ ∃𝑥∃𝑦 ∈ 𝐴 (𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥))
5		eluniab 4901	. . 3 ⊢ (𝑧 ∈ ∪ {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)} ↔ ∃𝑥(𝑧 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)))
6		eluni2 4891	. . . . . 6 ⊢ (𝑧 ∈ ∪ 𝐴 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝑦)
7	6	anbi1i 624	. . . . 5 ⊢ ((𝑧 ∈ ∪ 𝐴 ∧ 𝑧 ∈ 𝐵) ↔ (∃𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵))
8		elin 3947	. . . . 5 ⊢ (𝑧 ∈ (∪ 𝐴 ∩ 𝐵) ↔ (𝑧 ∈ ∪ 𝐴 ∧ 𝑧 ∈ 𝐵))
9		r19.41v 3176	. . . . 5 ⊢ (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵) ↔ (∃𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵))
10	7, 8, 9	3bitr4i 303	. . . 4 ⊢ (𝑧 ∈ (∪ 𝐴 ∩ 𝐵) ↔ ∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵))
11		vex 3467	. . . . . . . 8 ⊢ 𝑦 ∈ V
12	11	inex1 5297	. . . . . . 7 ⊢ (𝑦 ∩ 𝐵) ∈ V
13		eleq2 2822	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∩ 𝐵) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ (𝑦 ∩ 𝐵)))
14	12, 13	ceqsexv 3515	. . . . . 6 ⊢ (∃𝑥(𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥) ↔ 𝑧 ∈ (𝑦 ∩ 𝐵))
15		elin 3947	. . . . . 6 ⊢ (𝑧 ∈ (𝑦 ∩ 𝐵) ↔ (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵))
16	14, 15	bitri 275	. . . . 5 ⊢ (∃𝑥(𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵))
17	16	rexbii 3082	. . . 4 ⊢ (∃𝑦 ∈ 𝐴 ∃𝑥(𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵))
18		rexcom4 3272	. . . 4 ⊢ (∃𝑦 ∈ 𝐴 ∃𝑥(𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑥∃𝑦 ∈ 𝐴 (𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥))
19	10, 17, 18	3bitr2i 299	. . 3 ⊢ (𝑧 ∈ (∪ 𝐴 ∩ 𝐵) ↔ ∃𝑥∃𝑦 ∈ 𝐴 (𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥))
20	4, 5, 19	3bitr4ri 304	. 2 ⊢ (𝑧 ∈ (∪ 𝐴 ∩ 𝐵) ↔ 𝑧 ∈ ∪ {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)})
21	20	eqriv 2731	1 ⊢ (∪ 𝐴 ∩ 𝐵) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)}

Syntax hints:   ∧ wa 395   = wceq 1539  ∃wex 1778   ∈ wcel 2107  {cab 2712  ∃wrex 3059   ∩ cin 3930  ∪ cuni 4887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rex 3060  df-v 3465  df-in 3938  df-uni 4888

This theorem is referenced by: (None)