Metamath Proof Explorer
Description: Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007)
|
|
Ref |
Expression |
|
Assertion |
ssdifss |
⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∖ 𝐶 ) ⊆ 𝐵 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
difss |
⊢ ( 𝐴 ∖ 𝐶 ) ⊆ 𝐴 |
2 |
|
sstr |
⊢ ( ( ( 𝐴 ∖ 𝐶 ) ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∖ 𝐶 ) ⊆ 𝐵 ) |
3 |
1 2
|
mpan |
⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∖ 𝐶 ) ⊆ 𝐵 ) |