Metamath Proof Explorer

Theorem ttc0

Description: The transitive closure of the empty set is the empty set. (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion ttc0 
|- TC+ (/) = (/)

Proof

Step Hyp Ref Expression
1 tr0 
 |-  Tr (/)
2 ttctrid 
 |-  ( Tr (/) -> TC+ (/) = (/) )
3 1 2 ax-mp 
 |-  TC+ (/) = (/)