![]() |
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 4051 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 → ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶)) | |
2 | eliun 5001 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶) | |
3 | eliun 5001 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶) | |
4 | 1, 2, 3 | 3imtr4g 295 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶)) |
5 | 4 | ssrdv 3988 | 1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ∃wrex 3070 ⊆ wss 3948 ∪ ciun 4997 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rex 3071 df-v 3476 df-in 3955 df-ss 3965 df-iun 4999 |
This theorem is referenced by: iuneq1 5013 iunxdif2 5056 oelim2 8597 fsumiun 15771 ovolfiniun 25242 uniioovol 25320 fusgreghash2wspv 29843 esum2dlem 33376 esum2d 33377 carsgclctunlem2 33604 bnj1413 34332 bnj1408 34333 volsupnfl 36836 corclrcl 42760 cotrcltrcl 42778 iuneqfzuzlem 44343 fsumiunss 44590 sge0iunmptlemfi 45428 sge0iunmptlemre 45430 carageniuncllem1 45536 carageniuncllem2 45537 caratheodorylem2 45542 ovnsubaddlem1 45585 |
Copyright terms: Public domain | W3C validator |