| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > iunss1 | Structured version Visualization version GIF version | ||
| Description: Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| Ref | Expression |
|---|---|
| iunss1 | ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssrexv 4053 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 → ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶)) | |
| 2 | eliun 4995 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶) | |
| 3 | eliun 4995 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶) | |
| 4 | 1, 2, 3 | 3imtr4g 296 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶)) |
| 5 | 4 | ssrdv 3989 | 1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 ∃wrex 3070 ⊆ wss 3951 ∪ 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-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rex 3071 df-v 3482 df-ss 3968 df-iun 4993 |
| This theorem is referenced by: iuneq1 5008 iunxdif2 5053 oelim2 8633 fsumiun 15857 ovolfiniun 25536 uniioovol 25614 fusgreghash2wspv 30354 ssdifidllem 33484 esum2dlem 34093 esum2d 34094 carsgclctunlem2 34321 bnj1413 35049 bnj1408 35050 volsupnfl 37672 corclrcl 43720 cotrcltrcl 43738 iuneqfzuzlem 45345 fsumiunss 45590 sge0iunmptlemfi 46428 sge0iunmptlemre 46430 carageniuncllem1 46536 carageniuncllem2 46537 caratheodorylem2 46542 ovnsubaddlem1 46585 |
| Copyright terms: Public domain | W3C validator |