![]() |
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 3881 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | orim1d 964 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))) |
3 | elun 4050 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶)) | |
4 | elun 4050 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)) | |
5 | 2, 3, 4 | 3imtr4g 300 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) → 𝑥 ∈ (𝐵 ∪ 𝐶))) |
6 | 5 | ssrdv 3894 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∪ 𝐶) ⊆ (𝐵 ∪ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 845 ∈ wcel 2112 ∪ cun 3852 ⊆ wss 3854 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-ext 2730 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-tru 1542 df-ex 1783 df-sb 2071 df-clab 2737 df-cleq 2751 df-clel 2831 df-v 3409 df-un 3859 df-in 3861 df-ss 3871 |
This theorem is referenced by: unss2 4082 unss12 4083 eldifpw 7482 tposss 7896 dftpos4 7914 hashbclem 13845 incexclem 15224 mreexexlem2d 16959 catcoppccl 17419 neitr 21865 restntr 21867 leordtval2 21897 cmpcld 22087 uniioombllem3 24270 limcres 24570 plyss 24880 shlej1 29227 ss2mcls 33031 orderseqlem 33340 bj-rrhatsscchat 34916 pclfinclN 37511 |
Copyright terms: Public domain | W3C validator |