| 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 4915. (Contributed by David Moews, 1-May-2017.) |
| Ref | Expression |
|---|---|
| unissd.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
| Ref | Expression |
|---|---|
| unissd | ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | unissd.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
| 2 | uniss 4915 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ⊆ wss 3951 ∪ cuni 4907 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-uni 4908 |
| This theorem is referenced by: unieq 4918 dffv2 7004 onfununi 8381 fiuni 9468 dfac2a 10170 incexc 15873 incexc2 15874 isacs1i 17700 isacs3lem 18587 acsmapd 18599 acsmap2d 18600 dprdres 20048 dprd2da 20062 eltg3i 22968 unitg 22974 tgss 22975 tgcmp 23409 cmpfi 23416 alexsubALTlem4 24058 ptcmplem3 24062 ustbas2 24234 uniioombllem3 25620 madess 27915 shsupunss 31365 locfinref 33840 cmpcref 33849 dya2iocucvr 34286 omssubadd 34302 carsggect 34320 carsgclctun 34323 cvmscld 35278 fnemeet1 36367 fnejoin1 36369 onsucsuccmpi 36444 heibor1 37817 heiborlem10 37827 hbt 43142 pwsal 46330 prsal 46333 intsaluni 46344 caragenuni 46526 caragendifcl 46529 cnfsmf 46755 smfsssmf 46758 smfpimbor1lem2 46814 toplatglb 48890 setrecsss 49220 |
| Copyright terms: Public domain | W3C validator |