![]() |
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 4047 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 → ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶)) | |
2 | eliun 4995 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶) | |
3 | eliun 4995 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶) | |
4 | 1, 2, 3 | 3imtr4g 296 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶)) |
5 | 4 | ssrdv 3984 | 1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2099 ∃wrex 3065 ⊆ wss 3944 ∪ ciun 4991 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-rex 3066 df-v 3471 df-in 3951 df-ss 3961 df-iun 4993 |
This theorem is referenced by: iuneq1 5007 iunxdif2 5050 oelim2 8609 fsumiun 15793 ovolfiniun 25423 uniioovol 25501 fusgreghash2wspv 30138 esum2dlem 33701 esum2d 33702 carsgclctunlem2 33929 bnj1413 34656 bnj1408 34657 volsupnfl 37127 corclrcl 43109 cotrcltrcl 43127 iuneqfzuzlem 44688 fsumiunss 44935 sge0iunmptlemfi 45773 sge0iunmptlemre 45775 carageniuncllem1 45881 carageniuncllem2 45882 caratheodorylem2 45887 ovnsubaddlem1 45930 |
Copyright terms: Public domain | W3C validator |