|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > unss1 | Structured version Visualization version GIF version | ||
| Description: Subclass law for union of classes. (Contributed by NM, 14-Oct-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) | 
| Ref | Expression | 
|---|---|
| unss1 | ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ssel 3976 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
| 2 | 1 | orim1d 967 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))) | 
| 3 | elun 4152 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶)) | |
| 4 | elun 4152 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) | |
| 5 | 2, 3, 4 | 3imtr4g 296 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) → 𝑥 ∈ (𝐵 ∪ 𝐶))) | 
| 6 | 5 | ssrdv 3988 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∨ wo 847 ∈ wcel 2107 ∪ 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: unss2 4186 unss12 4187 eldifpw 7789 orderseqlem 8183 tposss 8253 dftpos4 8271 hashbclem 14492 incexclem 15873 mreexexlem2d 17689 catcoppccl 18163 neitr 23189 restntr 23191 leordtval2 23221 cmpcld 23411 uniioombllem3 25621 limcres 25922 plyss 26239 mulsproplem13 28155 mulsproplem14 28156 shlej1 31380 fineqvac 35112 ss2mcls 35574 bj-rrhatsscchat 37238 pclfinclN 39953 dmtposss 48782 | 
| Copyright terms: Public domain | W3C validator |