Theorem ttcsnmin

Description: The singleton transitive closure is the minimal transitive class containing A as an element. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcsnmin	|- ( ( A e. B /\ Tr B ) -> TC+ { A } C_ B )

Proof

Step	Hyp	Ref	Expression
1		snssi	|- ( A e. B -> { A } C_ B )
2		ttcmin	|- ( ( { A } C_ B /\ Tr B ) -> TC+ { A } C_ B )
3	1 2	sylan	|- ( ( A e. B /\ Tr B ) -> TC+ { A } C_ B )