Metamath Proof Explorer
Description: Subclass law for union of classes. Exercise 7 of TakeutiZaring p. 18.
(Contributed by NM, 14-Oct-1999)
|
|
Ref |
Expression |
|
Assertion |
unss2 |
⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ∪ 𝐴 ) ⊆ ( 𝐶 ∪ 𝐵 ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
unss1 |
⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∪ 𝐶 ) ⊆ ( 𝐵 ∪ 𝐶 ) ) |
2 |
|
uncom |
⊢ ( 𝐶 ∪ 𝐴 ) = ( 𝐴 ∪ 𝐶 ) |
3 |
|
uncom |
⊢ ( 𝐶 ∪ 𝐵 ) = ( 𝐵 ∪ 𝐶 ) |
4 |
1 2 3
|
3sstr4g |
⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ∪ 𝐴 ) ⊆ ( 𝐶 ∪ 𝐵 ) ) |