Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > iunxun | Structured version Visualization version GIF version |
Description: Separate a union in the index of an indexed union. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |
Ref | Expression |
---|---|
iunxun | ⊢ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 = (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexun 4090 | . . . 4 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝑦 ∈ 𝐶 ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ∨ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶)) | |
2 | eliun 4894 | . . . . 5 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶) | |
3 | eliun 4894 | . . . . 5 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶) | |
4 | 2, 3 | orbi12i 915 | . . . 4 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ∨ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶)) |
5 | 1, 4 | bitr4i 281 | . . 3 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝑦 ∈ 𝐶 ↔ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶)) |
6 | eliun 4894 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ ∃𝑥 ∈ (𝐴 ∪ 𝐵)𝑦 ∈ 𝐶) | |
7 | elun 4049 | . . 3 ⊢ (𝑦 ∈ (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶) ↔ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶)) | |
8 | 5, 6, 7 | 3bitr4i 306 | . 2 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ 𝑦 ∈ (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶)) |
9 | 8 | eqriv 2733 | 1 ⊢ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 = (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ∨ wo 847 = wceq 1543 ∈ wcel 2112 ∃wrex 3052 ∪ cun 3851 ∪ ciun 4890 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-ral 3056 df-rex 3057 df-v 3400 df-un 3858 df-iun 4892 |
This theorem is referenced by: iunxdif3 4989 iunxprg 4990 iunsuc 6273 funiunfv 7039 iunfi 8942 kmlem11 9739 ackbij1lem9 9807 fsum2dlem 15297 fsumiun 15348 fprod2dlem 15505 prmreclem4 16435 fiuncmp 22255 ovolfiniun 24352 finiunmbl 24395 volfiniun 24398 voliunlem1 24401 uniioombllem4 24437 iuninc 30573 iunxunsn 30579 iunxunpr 30580 ofpreima2 30677 indval2 31648 esum2dlem 31726 sigaclfu2 31755 fiunelros 31808 measvuni 31848 cvmliftlem10 32923 mrsubvrs 33151 mblfinlem2 35501 dfrcl4 40902 iunrelexp0 40928 comptiunov2i 40932 corclrcl 40933 trclfvdecomr 40954 dfrtrcl4 40964 corcltrcl 40965 cotrclrcl 40968 fiiuncl 42227 iunp1 42228 sge0iunmptlemfi 43569 ovolval4lem1 43805 |
Copyright terms: Public domain | W3C validator |