![]() |
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 4137 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶)) | |
2 | unss2 4139 | . 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷)) | |
3 | 1, 2 | sylan9ss 3955 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∪ cun 3906 ⊆ wss 3908 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3445 df-un 3913 df-in 3915 df-ss 3925 |
This theorem is referenced by: pwssun 5526 fun 6701 f1un 6801 undomOLD 8962 finsschain 9261 trclun 14853 relexpfld 14888 mulgfval 18827 mvdco 19180 dprd2da 19774 dmdprdsplit2lem 19777 lspun 20395 spanuni 30331 sshhococi 30333 mthmpps 34004 pibt2 35820 mblfinlem3 36049 dochdmj1 39785 mptrcllem 41790 clcnvlem 41800 dfrcl2 41851 relexpss1d 41882 corclrcl 41884 relexp0a 41893 corcltrcl 41916 frege131d 41941 |
Copyright terms: Public domain | W3C validator |