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 3960 | . . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵)) | |
2 | 1 | anim2d 611 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) |
3 | 2 | eximdv 1909 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))) |
4 | eluni 4835 | . . 3 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴)) | |
5 | eluni 4835 | . . 3 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) | |
6 | 3, 4, 5 | 3imtr4g 297 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ ∪ 𝐴 → 𝑥 ∈ ∪ 𝐵)) |
7 | 6 | ssrdv 3972 | 1 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∃wex 1771 ∈ wcel 2105 ⊆ wss 3935 ∪ cuni 4832 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3497 df-in 3942 df-ss 3951 df-uni 4833 |
This theorem is referenced by: unissi 4855 unissd 4856 intssuni2 4894 uniintsn 4906 relfld 6120 dffv2 6750 trcl 9159 cflm 9661 coflim 9672 cfslbn 9678 fin23lem41 9763 fin1a2lem12 9822 tskuni 10194 prdsval 16718 prdsbas 16720 prdsplusg 16721 prdsmulr 16722 prdsvsca 16723 prdshom 16730 mrcssv 16875 catcfuccl 17359 catcxpccl 17447 mrelatlub 17786 mreclatBAD 17787 dprdres 19081 dmdprdsplit2lem 19098 tgcl 21507 distop 21533 fctop 21542 cctop 21544 neiptoptop 21669 cmpcld 21940 uncmp 21941 cmpfi 21946 comppfsc 22070 kgentopon 22076 txcmplem2 22180 filconn 22421 alexsubALTlem3 22587 alexsubALT 22589 ptcmplem3 22592 dyadmbllem 24129 shsupcl 29043 hsupss 29046 shatomistici 30066 pwuniss 30234 carsggect 31476 carsgclctun 31479 cvmliftlem15 32443 filnetlem3 33626 icoreunrn 34523 ctbssinf 34570 pibt2 34581 heiborlem1 34972 lssats 36030 lpssat 36031 lssatle 36033 lssat 36034 dicval 38194 pwsal 42481 intsaluni 42493 |
Copyright terms: Public domain | W3C validator |