Metamath Proof Explorer

Theorem ttctr2

Description: The transitive closure of a class is transitive. (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion ttctr2 
|- ( A e. TC+ B -> A C_ TC+ B )

Proof

Step Hyp Ref Expression
1 ttctr 
 |-  Tr TC+ B
2 trss 
 |-  ( Tr TC+ B -> ( A e. TC+ B -> A C_ TC+ B ) )
3 1 2 ax-mp 
 |-  ( A e. TC+ B -> A C_ TC+ B )