![]() |
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 3972 | . . . . 5 ⊢ (𝐵 ⊆ 𝐶 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) | |
2 | 1 | ralimi 3073 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) |
3 | rexim 3077 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)) | |
4 | 2, 3 | syl 17 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)) |
5 | eliun 4997 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) | |
6 | eliun 4997 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶) | |
7 | 4, 5, 6 | 3imtr4g 295 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶)) |
8 | 7 | ssrdv 3984 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2099 ∀wral 3051 ∃wrex 3060 ⊆ wss 3946 ∪ ciun 4993 |
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 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ral 3052 df-rex 3061 df-v 3464 df-ss 3963 df-iun 4995 |
This theorem is referenced by: iuneq2 5012 abnexg 7756 oawordri 8572 omwordri 8594 oewordri 8614 oeworde 8615 r1val1 9822 cfslb2n 10302 imasaddvallem 17539 dprdss 20025 tgcmp 23393 txcmplem1 23633 txcmplem2 23634 xkococnlem 23651 alexsubALT 24043 ptcmplem3 24046 metnrmlem2 24864 uniiccvol 25597 dvfval 25914 gsumpart 32927 bnj1145 34851 bnj1136 34855 filnetlem3 36105 poimirlem32 37366 sstotbnd2 37488 equivtotbnd 37492 trclrelexplem 43415 corcltrcl 43443 cotrclrcl 43446 ovolval5lem2 46310 ovolval5lem3 46311 smflimsuplem7 46483 |
Copyright terms: Public domain | W3C validator |