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	⊢ ( ( 𝐴 ∈ 𝐵 ∧ Tr 𝐵 ) → TC+ { 𝐴 } ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		snssi	⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ⊆ 𝐵 )
2		ttcmin	⊢ ( ( { 𝐴 } ⊆ 𝐵 ∧ Tr 𝐵 ) → TC+ { 𝐴 } ⊆ 𝐵 )
3	1 2	sylan	⊢ ( ( 𝐴 ∈ 𝐵 ∧ Tr 𝐵 ) → TC+ { 𝐴 } ⊆ 𝐵 )