Metamath Proof Explorer

Theorem sstr2

Description: Transitivity of subclass relationship. Exercise 5 of TakeutiZaring p. 17. (Contributed by NM, 24-Jun-1993) (Proof shortened by Andrew Salmon, 14-Jun-2011)

Ref Expression
Assertion sstr2 ( 𝐴 ⊆ 𝐵 → ( 𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ssel ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
2 1 imim1d ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ) )
3 2 alimdv ⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶 ) → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ) )
4 dfss2 ⊢ ( 𝐵 ⊆ 𝐶 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶 ) )
5 dfss2 ⊢ ( 𝐴 ⊆ 𝐶 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) )
6 3 4 5 3imtr4g ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶 ) )