![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iunin2 | Structured version Visualization version GIF version |
Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 5066 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.) |
Ref | Expression |
---|---|
iunin2 | ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.42v 3181 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)) | |
2 | elin 3963 | . . . . 5 ⊢ (𝑦 ∈ (𝐵 ∩ 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) | |
3 | 2 | rexbii 3084 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ↔ ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) |
4 | eliun 5005 | . . . . 5 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶) | |
5 | 4 | anbi2i 621 | . . . 4 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)) |
6 | 1, 3, 5 | 3bitr4i 302 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶)) |
7 | eliun 5005 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ (𝐵 ∩ 𝐶)) | |
8 | elin 3963 | . . 3 ⊢ (𝑦 ∈ (𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶)) | |
9 | 6, 7, 8 | 3bitr4i 302 | . 2 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ↔ 𝑦 ∈ (𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶)) |
10 | 9 | eqriv 2723 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (𝐵 ∩ ∪ 𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 394 = wceq 1534 ∈ wcel 2099 ∃wrex 3060 ∩ cin 3946 ∪ ciun 5001 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rex 3061 df-v 3464 df-in 3954 df-iun 5003 |
This theorem is referenced by: iunin1 5080 2iunin 5084 resiun2 6010 infssuni 9388 kmlem11 10203 cmpsublem 23394 cmpsub 23395 kgentopon 23533 metnrmlem3 24868 ovoliunlem1 25522 voliunlem1 25570 voliunlem2 25571 uniioombllem2 25603 uniioombllem4 25606 volsup2 25625 itg1addlem5 25721 itg1climres 25735 uniin2 32473 carsgclctunlem2 34153 cvmscld 35101 cnambfre 37369 ftc1anclem6 37399 heiborlem3 37514 carageniuncllem2 46143 |
Copyright terms: Public domain | W3C validator |