Theorem ttcsng

Description: Relationship between TC+ { A } and TC+ A : the former contains the additional element A . (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcsng	|- ( A e. V -> TC+ { A } = ( TC+ A u. { A } ) )

Proof

Step	Hyp	Ref	Expression
1		ttciunun	|- TC+ { A } = ( U_ x e. { A } TC+ x u. { A } )
2		ttceq	|- ( x = A -> TC+ x = TC+ A )
3	2	iunxsng	|- ( A e. V -> U_ x e. { A } TC+ x = TC+ A )
4	3	uneq1d	|- ( A e. V -> ( U_ x e. { A } TC+ x u. { A } ) = ( TC+ A u. { A } ) )
5	1 4	eqtrid	|- ( A e. V -> TC+ { A } = ( TC+ A u. { A } ) )