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


Step Hyp Ref Expression
1 ssel A B x A x B
2 1 imim1d A B x B x C x A x C
3 2 alimdv A B x x B x C x x A x C
4 dfss2 B C x x B x C
5 dfss2 A C x x A x C
6 3 4 5 3imtr4g A B B C A C