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	Could not format assertion : No typesetting found for |- ( A e. V -> A e. TC+ { A } ) with typecode |-

Proof

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