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 3968 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 → ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶)) | |
2 | eliun 4908 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶) | |
3 | eliun 4908 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶) | |
4 | 1, 2, 3 | 3imtr4g 299 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶)) |
5 | 4 | ssrdv 3907 | 1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2110 ∃wrex 3062 ⊆ wss 3866 ∪ ciun 4904 |
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 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3066 df-rex 3067 df-v 3410 df-in 3873 df-ss 3883 df-iun 4906 |
This theorem is referenced by: iuneq1 4920 iunxdif2 4962 oelim2 8323 fsumiun 15385 ovolfiniun 24398 uniioovol 24476 fusgreghash2wspv 28418 esum2dlem 31772 esum2d 31773 carsgclctunlem2 31998 bnj1413 32728 bnj1408 32729 volsupnfl 35559 corclrcl 40992 cotrcltrcl 41010 iuneqfzuzlem 42546 fsumiunss 42791 sge0iunmptlemfi 43626 sge0iunmptlemre 43628 carageniuncllem1 43734 carageniuncllem2 43735 caratheodorylem2 43740 ovnsubaddlem1 43783 |
Copyright terms: Public domain | W3C validator |