|   | 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 4184 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶)) | |
| 2 | unss2 4186 | . 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷)) | |
| 3 | 1, 2 | sylan9ss 3996 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∪ cun 3948 ⊆ wss 3950 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-un 3955 df-ss 3967 | 
| This theorem is referenced by: pwssun 5574 fun 6769 f1un 6867 undomOLD 9101 finsschain 9400 trclun 15054 relexpfld 15089 mulgfval 19088 mvdco 19464 dprd2da 20063 dmdprdsplit2lem 20066 lspun 20986 mulsproplem13 28155 mulsproplem14 28156 spanuni 31564 sshhococi 31566 mthmpps 35588 pibt2 37419 mblfinlem3 37667 dochdmj1 41393 mptrcllem 43631 clcnvlem 43641 dfrcl2 43692 relexpss1d 43723 corclrcl 43725 relexp0a 43734 corcltrcl 43757 frege131d 43782 | 
| Copyright terms: Public domain | W3C validator |