Theorem ttcsnssg

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

	Ref	Expression
Assertion	ttcsnssg	Could not format assertion : No typesetting found for |- ( A e. V -> TC+ A C_ TC+ { A } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		snidg	$$⊢A\in V\to A\in \left\{A\right\}$$
2		ttcel2	Could not format ( A e. { A } -> TC+ A C_ TC+ { A } ) : No typesetting found for |- ( A e. { A } -> TC+ A C_ TC+ { A } ) with typecode |-
3	1 2	syl	Could not format ( A e. V -> TC+ A C_ TC+ { A } ) : No typesetting found for |- ( A e. V -> TC+ A C_ TC+ { A } ) with typecode |-