Metamath Proof Explorer

Theorem ttcel2

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

Ref Expression
Assertion ttcel2 
|- ( A e. B -> TC+ A C_ TC+ B )

Proof

Step Hyp Ref Expression
1 ttcid 
 |-  B C_ TC+ B
2 1 sseli 
 |-  ( A e. B -> A e. TC+ B )
3 ttcel 
 |-  ( A e. TC+ B -> TC+ A C_ TC+ B )
4 2 3 syl 
 |-  ( A e. B -> TC+ A C_ TC+ B )