Metamath Proof Explorer

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 
|- ( A e. V -> A e. TC+ { A } )

Proof

Step Hyp Ref Expression
1 ttcid 
 |-  { A } C_ TC+ { A }
2 snidg 
 |-  ( A e. V -> A e. { A } )
3 1 2 sselid 
 |-  ( A e. V -> A e. TC+ { A } )