| 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 4864. (Contributed by David Moews, 1-May-2017.) |
| Ref | Expression |
|---|---|
| unissd.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
| Ref | Expression |
|---|---|
| unissd | ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | unissd.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
| 2 | uniss 4864 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝐴 ⊆ ∪ 𝐵) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ⊆ wss 3897 ∪ cuni 4856 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-ext 2703 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1544 df-ex 1781 df-sb 2068 df-clab 2710 df-cleq 2723 df-clel 2806 df-v 3438 df-ss 3914 df-uni 4857 |
| This theorem is referenced by: unieq 4867 dffv2 6917 onfununi 8261 fiuni 9312 dfac2a 10021 incexc 15744 incexc2 15745 isacs1i 17563 isacs3lem 18448 acsmapd 18460 acsmap2d 18461 dprdres 19942 dprd2da 19956 eltg3i 22876 unitg 22882 tgss 22883 tgcmp 23316 cmpfi 23323 alexsubALTlem4 23965 ptcmplem3 23969 ustbas2 24140 uniioombllem3 25513 madess 27821 oldss 27823 shsupunss 31326 locfinref 33854 cmpcref 33863 dya2iocucvr 34297 omssubadd 34313 carsggect 34331 carsgclctun 34334 cvmscld 35317 fnemeet1 36410 fnejoin1 36412 onsucsuccmpi 36487 heibor1 37849 heiborlem10 37859 hbt 43222 pwsal 46412 prsal 46415 intsaluni 46426 caragenuni 46608 caragendifcl 46611 cnfsmf 46837 smfsssmf 46840 smfpimbor1lem2 46896 toplatglb 49100 setrecsss 49801 |
| Copyright terms: Public domain | W3C validator |