Theorem inuni 5356

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 3187	. . . . 5 ⊢ (∃𝑦 ∈ 𝐴 (𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥) ↔ (∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥))
3	1, 2	bitr4i 278	. . . 4 ⊢ ((𝑧 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)) ↔ ∃𝑦 ∈ 𝐴 (𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥))
4	3	exbii 1845	. . 3 ⊢ (∃𝑥(𝑧 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)) ↔ ∃𝑥∃𝑦 ∈ 𝐴 (𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥))
5		eluniab 4926	. . 3 ⊢ (𝑧 ∈ ∪ {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)} ↔ ∃𝑥(𝑧 ∈ 𝑥 ∧ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)))
6		eluni2 4916	. . . . . 6 ⊢ (𝑧 ∈ ∪ 𝐴 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝑦)
7	6	anbi1i 624	. . . . 5 ⊢ ((𝑧 ∈ ∪ 𝐴 ∧ 𝑧 ∈ 𝐵) ↔ (∃𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵))
8		elin 3979	. . . . 5 ⊢ (𝑧 ∈ (∪ 𝐴 ∩ 𝐵) ↔ (𝑧 ∈ ∪ 𝐴 ∧ 𝑧 ∈ 𝐵))
9		r19.41v 3187	. . . . 5 ⊢ (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵) ↔ (∃𝑦 ∈ 𝐴 𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵))
10	7, 8, 9	3bitr4i 303	. . . 4 ⊢ (𝑧 ∈ (∪ 𝐴 ∩ 𝐵) ↔ ∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵))
11		vex 3482	. . . . . . . 8 ⊢ 𝑦 ∈ V
12	11	inex1 5323	. . . . . . 7 ⊢ (𝑦 ∩ 𝐵) ∈ V
13		eleq2 2828	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∩ 𝐵) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ (𝑦 ∩ 𝐵)))
14	12, 13	ceqsexv 3530	. . . . . 6 ⊢ (∃𝑥(𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥) ↔ 𝑧 ∈ (𝑦 ∩ 𝐵))
15		elin 3979	. . . . . 6 ⊢ (𝑧 ∈ (𝑦 ∩ 𝐵) ↔ (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵))
16	14, 15	bitri 275	. . . . 5 ⊢ (∃𝑥(𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥) ↔ (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵))
17	16	rexbii 3092	. . . 4 ⊢ (∃𝑦 ∈ 𝐴 ∃𝑥(𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝐵))
18		rexcom4 3286	. . . 4 ⊢ (∃𝑦 ∈ 𝐴 ∃𝑥(𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥) ↔ ∃𝑥∃𝑦 ∈ 𝐴 (𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥))
19	10, 17, 18	3bitr2i 299	. . 3 ⊢ (𝑧 ∈ (∪ 𝐴 ∩ 𝐵) ↔ ∃𝑥∃𝑦 ∈ 𝐴 (𝑥 = (𝑦 ∩ 𝐵) ∧ 𝑧 ∈ 𝑥))
20	4, 5, 19	3bitr4ri 304	. 2 ⊢ (𝑧 ∈ (∪ 𝐴 ∩ 𝐵) ↔ 𝑧 ∈ ∪ {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)})
21	20	eqriv 2732	1 ⊢ (∪ 𝐴 ∩ 𝐵) = ∪ {𝑥 ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 ∩ 𝐵)}

Syntax hints:   ∧ wa 395   = wceq 1537  ∃wex 1776   ∈ wcel 2106  {cab 2712  ∃wrex 3068   ∩ cin 3962  ∪ cuni 4912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rex 3069  df-v 3480  df-in 3970  df-uni 4913

This theorem is referenced by: (None)