Theorem ttcel2

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

	Ref	Expression
Assertion	ttcel2	Could not format assertion : No typesetting found for |- ( A e. B -> TC+ A C_ TC+ B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ttcid	Could not format B C_ TC+ B : No typesetting found for |- B C_ TC+ B with typecode |-
2	1	sseli	Could not format ( A e. B -> A e. TC+ B ) : No typesetting found for |- ( A e. B -> A e. TC+ B ) with typecode |-
3		ttcel	Could not format ( A e. TC+ B -> TC+ A C_ TC+ B ) : No typesetting found for |- ( A e. TC+ B -> TC+ A C_ TC+ B ) with typecode |-
4	2 3	syl	Could not format ( A e. B -> TC+ A C_ TC+ B ) : No typesetting found for |- ( A e. B -> TC+ A C_ TC+ B ) with typecode |-