Metamath Proof Explorer

Theorem ssrin

Description: Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion ssrin ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∩ 𝐶 ) ⊆ ( 𝐵 ∩ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ssel ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
2 1 anim1d ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
3 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) )
4 elin ⊢ ( 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) )
5 2 3 4 3imtr4g ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) → 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ) )
6 5 ssrdv ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∩ 𝐶 ) ⊆ ( 𝐵 ∩ 𝐶 ) )