Metamath Proof Explorer

Theorem trss

Description: An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994) (Proof shortened by JJ, 26-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 dftr3 
 |-  ( Tr A <-> A. x e. A x C_ A )
2 sseq1 
 |-  ( x = B -> ( x C_ A <-> B C_ A ) )
3 2 rspccv 
 |-  ( A. x e. A x C_ A -> ( B e. A -> B C_ A ) )
4 1 3 sylbi 
 |-  ( Tr A -> ( B e. A -> B C_ A ) )