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

Proof

Step	Hyp	Ref	Expression
1		ttciunun	⊢ TC+ { 𝐴 } = ( ∪ 𝑥 ∈ { 𝐴 } TC+ 𝑥 ∪ { 𝐴 } )
2		ttceq	⊢ ( 𝑥 = 𝐴 → TC+ 𝑥 = TC+ 𝐴 )
3	2	iunxsng	⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝑥 ∈ { 𝐴 } TC+ 𝑥 = TC+ 𝐴 )
4	3	uneq1d	⊢ ( 𝐴 ∈ 𝑉 → ( ∪ 𝑥 ∈ { 𝐴 } TC+ 𝑥 ∪ { 𝐴 } ) = ( TC+ 𝐴 ∪ { 𝐴 } ) )
5	1 4	eqtrid	⊢ ( 𝐴 ∈ 𝑉 → TC+ { 𝐴 } = ( TC+ 𝐴 ∪ { 𝐴 } ) )