Metamath Proof Explorer

Theorem ttctr3

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

Ref Expression
Assertion ttctr3 
|- U. TC+ A C_ TC+ A

Proof

Step Hyp Ref Expression
1 ttctr 
 |-  Tr TC+ A
2 df-tr 
 |-  ( Tr TC+ A <-> U. TC+ A C_ TC+ A )
3 1 2 mpbi 
 |-  U. TC+ A C_ TC+ A