Theorem ttcsnssg

Description: The transitive closure is contained in the singleton transitive closure. (Contributed by Matthew House, 6-Apr-2026)

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

Proof

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