Theorem iunin2 4995

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

Syntax hints:   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∃wrex 3141   ∩ cin 3937  ∪ ciun 4921

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-v 3498  df-in 3945  df-iun 4923

This theorem is referenced by:  iunin1  4996  2iunin  5000  resiun2  5876  infssuni  8817  kmlem11  9588  cmpsublem  22009  cmpsub  22010  kgentopon  22148  metnrmlem3  23471  ovoliunlem1  24105  voliunlem1  24153  voliunlem2  24154  uniioombllem2  24186  uniioombllem4  24189  volsup2  24208  itg1addlem5  24303  itg1climres  24317  uniin2  30306  carsgclctunlem2  31579  cvmscld  32522  cnambfre  34942  ftc1anclem6  34974  heiborlem3  35093  carageniuncllem2  42811