Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > unss12 | Structured version Visualization version GIF version |
Description: Subclass law for union of classes. (Contributed by NM, 2-Jun-2004.) |
Ref | Expression |
---|---|
unss12 | ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unss1 4079 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶)) | |
2 | unss2 4081 | . 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷)) | |
3 | 1, 2 | sylan9ss 3900 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∪ cun 3851 ⊆ wss 3853 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-v 3400 df-un 3858 df-in 3860 df-ss 3870 |
This theorem is referenced by: pwssun 5436 fun 6559 undom 8711 finsschain 8961 trclun 14542 relexpfld 14577 mulgfval 18444 mvdco 18791 dprd2da 19383 dmdprdsplit2lem 19386 lspun 19978 spanuni 29579 sshhococi 29581 mthmpps 33211 pibt2 35274 mblfinlem3 35502 dochdmj1 39090 mptrcllem 40838 clcnvlem 40848 dfrcl2 40900 relexpss1d 40931 corclrcl 40933 relexp0a 40942 corcltrcl 40965 frege131d 40990 |
Copyright terms: Public domain | W3C validator |