Metamath Proof Explorer
Description: Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999)
|
|
Ref |
Expression |
|
Assertion |
ssinss1 |
⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
inss1 |
⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 |
2 |
|
sstr2 |
⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 → ( 𝐴 ⊆ 𝐶 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ) ) |
3 |
1 2
|
ax-mp |
⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ) |