Theorem ttcsnidg

Description: The singleton transitive closure contains its argument A as an element. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcsnidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ TC+ { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		ttcid	⊢ { 𝐴 } ⊆ TC+ { 𝐴 }
2		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
3	1 2	sselid	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ TC+ { 𝐴 } )