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

Proof

Step	Hyp	Ref	Expression
1		snssi	$$⊢A\in B\to \left\{A\right\}\subseteq B$$
2		ttcmin	Could not format ( ( { A } C_ B /\ Tr B ) -> TC+ { A } C_ B ) : No typesetting found for |- ( ( { A } C_ B /\ Tr B ) -> TC+ { A } C_ B ) with typecode |-
3	1 2	sylan	Could not format ( ( A e. B /\ Tr B ) -> TC+ { A } C_ B ) : No typesetting found for |- ( ( A e. B /\ Tr B ) -> TC+ { A } C_ B ) with typecode |-