![]() |
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 3950 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 → ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶)) | |
2 | eliun 4823 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶) | |
3 | eliun 4823 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶) | |
4 | 1, 2, 3 | 3imtr4g 297 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶)) |
5 | 4 | ssrdv 3890 | 1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2079 ∃wrex 3104 ⊆ wss 3854 ∪ ciun 4819 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-ext 2767 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ral 3108 df-rex 3109 df-v 3434 df-in 3861 df-ss 3869 df-iun 4821 |
This theorem is referenced by: iuneq1 4834 iunxdif2 4870 oelim2 8062 fsumiun 14997 ovolfiniun 23773 uniioovol 23851 fusgreghash2wspv 27794 esum2dlem 30924 esum2d 30925 carsgclctunlem2 31150 bnj1413 31877 bnj1408 31878 volsupnfl 34414 corclrcl 39488 cotrcltrcl 39506 iuneqfzuzlem 41096 fsumiunss 41352 sge0iunmptlemfi 42191 sge0iunmptlemre 42193 carageniuncllem1 42299 carageniuncllem2 42300 caratheodorylem2 42305 ovnsubaddlem1 42348 |
Copyright terms: Public domain | W3C validator |