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	Could not format assertion : No typesetting found for |- ( A e. V -> TC+ A = ( TC ` A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ttcexg	Could not format ( A e. V -> TC+ A e. _V ) : No typesetting found for |- ( A e. V -> TC+ A e. _V ) with typecode |-
2		dfttc3gw	Could not format ( TC+ A e. _V -> TC+ A = ( TC ` A ) ) : No typesetting found for |- ( TC+ A e. _V -> TC+ A = ( TC ` A ) ) with typecode |-
3	1 2	syl	Could not format ( A e. V -> TC+ A = ( TC ` A ) ) : No typesetting found for |- ( A e. V -> TC+ A = ( TC ` A ) ) with typecode |-