Theorem iunin2 5013

Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 5001 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 3169	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶))
2		elin 3905	. . . . 5 ⊢ (𝑦 ∈ (𝐵 ∩ 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))
3	2	rexbii 3084	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ↔ ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))
4		eliun 4937	. . . . 5 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)
5	4	anbi2i 624	. . . 4 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶))
6	1, 3, 5	3bitr4i 303	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶))
7		eliun 4937	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶))
8		elin 3905	. . 3 ⊢ (𝑦 ∈ (𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶))
9	6, 7, 8	3bitr4i 303	. 2 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶))
10	9	eqriv 2733	1 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3061   ∩ cin 3888  ∪ ciun 4933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-v 3431  df-in 3896  df-iun 4935

This theorem is referenced by:  iunin1  5014  2iunin  5018  resiun2  5965  infssuni  9256  kmlem11  10083  cmpsublem  23364  cmpsub  23365  kgentopon  23503  metnrmlem3  24827  ovoliunlem1  25469  voliunlem1  25517  voliunlem2  25518  uniioombllem2  25550  uniioombllem4  25553  volsup2  25572  itg1addlem5  25667  itg1climres  25681  uniin2  32622  carsgclctunlem2  34463  cvmscld  35455  cnambfre  37989  ftc1anclem6  38019  heiborlem3  38134  carageniuncllem2  46950