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 A B B C A C

Proof

Step Hyp Ref Expression
1 imim1 x A x B x B x C x A x C
2 1 al2imi x x A x B x x B x C x x A x C
3 df-ss A B x x A x B
4 df-ss B C x x B x C
5 df-ss A C x x A x C
6 4 5 imbi12i B C A C x x B x C x x A x C
7 2 3 6 3imtr4i A B B C A C