Theorem iunin2 5021

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∃wrex 3057   ∩ cin 3897  ∪ ciun 4941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rex 3058  df-v 3439  df-in 3905  df-iun 4943

This theorem is referenced by:  iunin1  5022  2iunin  5026  resiun2  5953  infssuni  9237  kmlem11  10059  cmpsublem  23315  cmpsub  23316  kgentopon  23454  metnrmlem3  24778  ovoliunlem1  25431  voliunlem1  25479  voliunlem2  25480  uniioombllem2  25512  uniioombllem4  25515  volsup2  25534  itg1addlem5  25629  itg1climres  25643  uniin2  32534  carsgclctunlem2  34353  cvmscld  35338  cnambfre  37728  ftc1anclem6  37758  heiborlem3  37873  carageniuncllem2  46644