Theorem ttcel2

Description: Elements turn into subclasses upon taking transitive closures. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcel2	⊢ ( 𝐴 ∈ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ttcid	⊢ 𝐵 ⊆ TC+ 𝐵
2	1	sseli	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ TC+ 𝐵 )
3		ttcel	⊢ ( 𝐴 ∈ TC+ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵 )
4	2 3	syl	⊢ ( 𝐴 ∈ 𝐵 → TC+ 𝐴 ⊆ TC+ 𝐵 )