Metamath Proof Explorer
Description: Add left intersection to subclass relation. (Contributed by NM, 19Oct1999)


Ref 
Expression 

Assertion 
sslin 
⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ∩ 𝐴 ) ⊆ ( 𝐶 ∩ 𝐵 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

ssrin 
⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∩ 𝐶 ) ⊆ ( 𝐵 ∩ 𝐶 ) ) 
2 

incom 
⊢ ( 𝐶 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐶 ) 
3 

incom 
⊢ ( 𝐶 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐶 ) 
4 
1 2 3

3sstr4g 
⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ∩ 𝐴 ) ⊆ ( 𝐶 ∩ 𝐵 ) ) 