![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > uniss | Structured version Visualization version GIF version |
Description: Subclass relationship for class union. Theorem 61 of [Suppes] p. 39. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Ref | Expression |
---|---|
uniss | ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel 3630 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵)) | |
2 | 1 | anim2d 588 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) |
3 | 2 | eximdv 1886 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) |
4 | eluni 4471 | . . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) | |
5 | eluni 4471 | . . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) | |
6 | 3, 4, 5 | 3imtr4g 285 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵)) |
7 | 6 | ssrdv 3642 | 1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∃wex 1744 ∈ wcel 2030 ⊆ wss 3607 ∪ cuni 4468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-in 3614 df-ss 3621 df-uni 4469 |
This theorem is referenced by: unissi 4493 unissd 4494 intssuni2 4534 uniintsn 4546 relfld 5699 dffv2 6310 trcl 8642 cflm 9110 coflim 9121 cfslbn 9127 fin23lem41 9212 fin1a2lem12 9271 tskuni 9643 prdsval 16162 prdsbas 16164 prdsplusg 16165 prdsmulr 16166 prdsvsca 16167 prdshom 16174 mrcssv 16321 catcfuccl 16806 catcxpccl 16894 mrelatlub 17233 mreclatBAD 17234 dprdres 18473 dmdprdsplit2lem 18490 tgcl 20821 distop 20847 fctop 20856 cctop 20858 neiptoptop 20983 cmpcld 21253 uncmp 21254 cmpfi 21259 comppfsc 21383 kgentopon 21389 txcmplem2 21493 filconn 21734 alexsubALTlem3 21900 alexsubALT 21902 ptcmplem3 21905 dyadmbllem 23413 shsupcl 28325 hsupss 28328 shatomistici 29348 pwuniss 29496 carsggect 30508 carsgclctun 30511 cvmliftlem15 31406 frrlem5c 31911 filnetlem3 32500 icoreunrn 33337 heiborlem1 33740 lssats 34617 lpssat 34618 lssatle 34620 lssat 34621 dicval 36782 pwsal 40853 prsal 40856 intsaluni 40865 |
Copyright terms: Public domain | W3C validator |