Theorem iunin2 5038

Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 5025 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.)

Assertion

Ref	Expression
iunin2	⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶)

Distinct variable group:   𝑥,𝐵

Allowed substitution hints:   𝐴(𝑥)   𝐶(𝑥)

Proof of Theorem iunin2

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		r19.42v 3170	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶))
2		elin 3933	. . . . 5 ⊢ (𝑦 ∈ (𝐵 ∩ 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))
3	2	rexbii 3077	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ↔ ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))
4		eliun 4962	. . . . 5 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)
5	4	anbi2i 623	. . . 4 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶))
6	1, 3, 5	3bitr4i 303	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶))
7		eliun 4962	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))
8		elin 3933	. . 3 ⊢ (𝑦 ∈ (𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶))
9	6, 7, 8	3bitr4i 303	. 2 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶))
10	9	eqriv 2727	1 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3054   ∩ cin 3916  ∪ ciun 4958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-v 3452  df-in 3924  df-iun 4960

This theorem is referenced by:  iunin1  5039  2iunin  5043  resiun2  5974  infssuni  9304  kmlem11  10121  cmpsublem  23293  cmpsub  23294  kgentopon  23432  metnrmlem3  24757  ovoliunlem1  25410  voliunlem1  25458  voliunlem2  25459  uniioombllem2  25491  uniioombllem4  25494  volsup2  25513  itg1addlem5  25608  itg1climres  25622  uniin2  32488  carsgclctunlem2  34317  cvmscld  35267  cnambfre  37669  ftc1anclem6  37699  heiborlem3  37814  carageniuncllem2  46527