Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > unissd | Structured version Visualization version GIF version |
Description: Subclass relationship for subclass union. Deduction form of uniss 4394. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
unissd.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Ref | Expression |
---|---|
unissd | ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unissd.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | uniss 4394 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3540 ∪ cuni 4372 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-in 3547 df-ss 3554 df-uni 4373 |
This theorem is referenced by: dffv2 6181 onfununi 7325 fiuni 8217 dfac2a 8835 incexc 14408 incexc2 14409 isacs1i 16141 isacs3lem 16989 acsmapd 17001 acsmap2d 17002 dprdres 18250 dprd2da 18264 eltg3i 20576 unitg 20582 tgss 20583 tgcmp 21014 cmpfi 21021 alexsubALTlem4 21664 ptcmplem3 21668 ustbas2 21839 uniioombllem3 23159 shsupunss 27589 locfinref 29236 cmpcref 29245 dya2iocucvr 29673 omssubadd 29689 carsggect 29707 cvmscld 30509 nofulllem3 31103 fnemeet1 31531 fnejoin1 31533 onsucsuccmpi 31612 heibor1 32779 heiborlem10 32789 hbt 36719 caragenuni 39401 caragendifcl 39404 cnfsmf 39627 smfsssmf 39630 smfpimbor1lem2 39684 |
Copyright terms: Public domain | W3C validator |