![]() |
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 4195 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶)) | |
2 | unss2 4197 | . 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷)) | |
3 | 1, 2 | sylan9ss 4009 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∪ cun 3961 ⊆ wss 3963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-un 3968 df-ss 3980 |
This theorem is referenced by: pwssun 5580 fun 6771 f1un 6869 undomOLD 9099 finsschain 9397 trclun 15050 relexpfld 15085 mulgfval 19100 mvdco 19478 dprd2da 20077 dmdprdsplit2lem 20080 lspun 21003 mulsproplem13 28169 mulsproplem14 28170 spanuni 31573 sshhococi 31575 mthmpps 35567 pibt2 37400 mblfinlem3 37646 dochdmj1 41373 mptrcllem 43603 clcnvlem 43613 dfrcl2 43664 relexpss1d 43695 corclrcl 43697 relexp0a 43706 corcltrcl 43729 frege131d 43754 |
Copyright terms: Public domain | W3C validator |