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) Avoid axioms. (Revised by GG, 19-May-2025)

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

Proof

Step Hyp Ref Expression
1 imim1 ( ( 𝑥𝐴𝑥𝐵 ) → ( ( 𝑥𝐵𝑥𝐶 ) → ( 𝑥𝐴𝑥𝐶 ) ) )
2 1 al2imi ( ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) → ( ∀ 𝑥 ( 𝑥𝐵𝑥𝐶 ) → ∀ 𝑥 ( 𝑥𝐴𝑥𝐶 ) ) )
3 df-ss ( 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) )
4 df-ss ( 𝐵𝐶 ↔ ∀ 𝑥 ( 𝑥𝐵𝑥𝐶 ) )
5 df-ss ( 𝐴𝐶 ↔ ∀ 𝑥 ( 𝑥𝐴𝑥𝐶 ) )
6 4 5 imbi12i ( ( 𝐵𝐶𝐴𝐶 ) ↔ ( ∀ 𝑥 ( 𝑥𝐵𝑥𝐶 ) → ∀ 𝑥 ( 𝑥𝐴𝑥𝐶 ) ) )
7 2 3 6 3imtr4i ( 𝐴𝐵 → ( 𝐵𝐶𝐴𝐶 ) )