![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ss2iun | Structured version Visualization version GIF version |
Description: Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Ref | Expression |
---|---|
ss2iun | ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3936 | . . . . 5 ⊢ (𝐵 ⊆ 𝐶 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) | |
2 | 1 | ralimi 3085 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) |
3 | rexim 3089 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)) | |
4 | 2, 3 | syl 17 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)) |
5 | eliun 4957 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) | |
6 | eliun 4957 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶) | |
7 | 4, 5, 6 | 3imtr4g 295 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶)) |
8 | 7 | ssrdv 3949 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ∀wral 3063 ∃wrex 3072 ⊆ wss 3909 ∪ ciun 4953 |
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 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ral 3064 df-rex 3073 df-v 3446 df-in 3916 df-ss 3926 df-iun 4955 |
This theorem is referenced by: iuneq2 4972 abnexg 7687 oawordri 8494 omwordri 8516 oewordri 8536 oeworde 8537 r1val1 9719 cfslb2n 10201 imasaddvallem 17408 dprdss 19804 tgcmp 22748 txcmplem1 22988 txcmplem2 22989 xkococnlem 23006 alexsubALT 23398 ptcmplem3 23401 metnrmlem2 24219 uniiccvol 24940 dvfval 25257 gsumpart 31792 bnj1145 33496 bnj1136 33500 filnetlem3 34841 poimirlem32 36099 sstotbnd2 36222 equivtotbnd 36226 trclrelexplem 41963 corcltrcl 41991 cotrclrcl 41994 ovolval5lem2 44864 ovolval5lem3 44865 smflimsuplem7 45037 |
Copyright terms: Public domain | W3C validator |