Metamath Proof Explorer

Theorem dfttc3g

Description: The transitive closure of a set A is ( TCA ) , assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion dfttc3g 
|- ( A e. V -> TC+ A = ( TC ` A ) )

Proof

Step Hyp Ref Expression
1 ttcexg 
 |-  ( A e. V -> TC+ A e. _V )
2 dfttc3gw 
 |-  ( TC+ A e. _V -> TC+ A = ( TC ` A ) )
3 1 2 syl 
 |-  ( A e. V -> TC+ A = ( TC ` A ) )