| 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 4196 | . . . 4 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝑦 ∈ 𝐶 ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ∨ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶)) | |
| 2 | eliun 4995 | . . . . 5 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶) | |
| 3 | eliun 4995 | . . . . 5 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶) | |
| 4 | 2, 3 | orbi12i 915 | . . . 4 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ∨ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶)) |
| 5 | 1, 4 | bitr4i 278 | . . 3 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝑦 ∈ 𝐶 ↔ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶)) |
| 6 | eliun 4995 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ ∃𝑥 ∈ (𝐴 ∪ 𝐵)𝑦 ∈ 𝐶) | |
| 7 | elun 4153 | . . 3 ⊢ (𝑦 ∈ (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶) ↔ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶)) | |
| 8 | 5, 6, 7 | 3bitr4i 303 | . 2 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ 𝑦 ∈ (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶)) |
| 9 | 8 | eqriv 2734 | 1 ⊢ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 = (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: ∨ wo 848 = wceq 1540 ∈ wcel 2108 ∃wrex 3070 ∪ cun 3949 ∪ ciun 4991 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rex 3071 df-v 3482 df-un 3956 df-iun 4993 |
| This theorem is referenced by: iunxdif3 5095 iunxprg 5096 iunsuc 6469 funiunfv 7268 iunfi 9383 kmlem11 10201 ackbij1lem9 10267 fsum2dlem 15806 fsumiun 15857 fprod2dlem 16016 prmreclem4 16957 fiuncmp 23412 ovolfiniun 25536 finiunmbl 25579 volfiniun 25582 voliunlem1 25585 uniioombllem4 25621 iuninc 32573 iunxunsn 32579 iunxunpr 32580 ofpreima2 32676 indval2 32839 esum2dlem 34093 sigaclfu2 34122 fiunelros 34175 measvuni 34215 cvmliftlem10 35299 mrsubvrs 35527 mblfinlem2 37665 dfrcl4 43689 iunrelexp0 43715 comptiunov2i 43719 corclrcl 43720 trclfvdecomr 43741 dfrtrcl4 43751 corcltrcl 43752 cotrclrcl 43755 fiiuncl 45070 iunp1 45071 sge0iunmptlemfi 46428 ovolval4lem1 46664 |
| Copyright terms: Public domain | W3C validator |