Metamath Proof Explorer

Theorem trsucss

Description: A member of the successor of a transitive class is a subclass of it. Lemma 1.13 of Schloeder p. 2. (Contributed by NM, 4-Oct-2003)

Ref Expression
Assertion trsucss 
|- ( Tr A -> ( B e. suc A -> B C_ A ) )

Proof

Step Hyp Ref Expression
1 elsuci 
 |-  ( B e. suc A -> ( B e. A \/ B = A ) )
2 trss 
 |-  ( Tr A -> ( B e. A -> B C_ A ) )
3 eqimss 
 |-  ( B = A -> B C_ A )
4 3 a1i 
 |-  ( Tr A -> ( B = A -> B C_ A ) )
5 2 4 jaod 
 |-  ( Tr A -> ( ( B e. A \/ B = A ) -> B C_ A ) )
6 1 5 syl5 
 |-  ( Tr A -> ( B e. suc A -> B C_ A ) )