# 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}\subseteq {B}\to \left({B}\subseteq {C}\to {A}\subseteq {C}\right)$

### Proof

Step Hyp Ref Expression
1 ssel ${⊢}{A}\subseteq {B}\to \left({x}\in {A}\to {x}\in {B}\right)$
2 1 imim1d ${⊢}{A}\subseteq {B}\to \left(\left({x}\in {B}\to {x}\in {C}\right)\to \left({x}\in {A}\to {x}\in {C}\right)\right)$
3 2 alimdv ${⊢}{A}\subseteq {B}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to {x}\in {C}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {C}\right)\right)$
4 dfss2 ${⊢}{B}\subseteq {C}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to {x}\in {C}\right)$
5 dfss2 ${⊢}{A}\subseteq {C}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {C}\right)$
6 3 4 5 3imtr4g ${⊢}{A}\subseteq {B}\to \left({B}\subseteq {C}\to {A}\subseteq {C}\right)$