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	⊢ ( 𝐴 ∈ 𝑉 → TC+ 𝐴 = ( TC ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ttcexg	⊢ ( 𝐴 ∈ 𝑉 → TC+ 𝐴 ∈ V )
2		dfttc3gw	⊢ ( TC+ 𝐴 ∈ V → TC+ 𝐴 = ( TC ‘ 𝐴 ) )
3	1 2	syl	⊢ ( 𝐴 ∈ 𝑉 → TC+ 𝐴 = ( TC ‘ 𝐴 ) )