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 3597 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵)) | |
2 | 1 | anim2d 589 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) |
3 | 2 | eximdv 1846 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) |
4 | eluni 4439 | . . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) | |
5 | eluni 4439 | . . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) | |
6 | 3, 4, 5 | 3imtr4g 285 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵)) |
7 | 6 | ssrdv 3609 | 1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∃wex 1704 ∈ wcel 1990 ⊆ wss 3574 ∪ cuni 4436 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-in 3581 df-ss 3588 df-uni 4437 |
This theorem is referenced by: unissi 4461 unissd 4462 intssuni2 4502 uniintsn 4514 relfld 5661 dffv2 6271 trcl 8604 cflm 9072 coflim 9083 cfslbn 9089 fin23lem41 9174 fin1a2lem12 9233 tskuni 9605 prdsval 16115 prdsbas 16117 prdsplusg 16118 prdsmulr 16119 prdsvsca 16120 prdshom 16127 mrcssv 16274 catcfuccl 16759 catcxpccl 16847 mrelatlub 17186 mreclatBAD 17187 dprdres 18427 dmdprdsplit2lem 18444 tgcl 20773 distop 20799 fctop 20808 cctop 20810 neiptoptop 20935 cmpcld 21205 uncmp 21206 cmpfi 21211 comppfsc 21335 kgentopon 21341 txcmplem2 21445 filconn 21687 alexsubALTlem3 21853 alexsubALT 21855 ptcmplem3 21858 dyadmbllem 23367 shsupcl 28197 hsupss 28200 shatomistici 29220 pwuniss 29370 carsggect 30380 carsgclctun 30383 cvmliftlem15 31280 frrlem5c 31786 filnetlem3 32375 icoreunrn 33207 heiborlem1 33610 lssats 34299 lpssat 34300 lssatle 34302 lssat 34303 dicval 36465 pwsal 40535 prsal 40538 intsaluni 40547 |
Copyright terms: Public domain | W3C validator |