Theorem ttcexrg

Description: If the transitive closure of a class is a set, then the class is a set. (Contributed by Matthew House, 6-Apr-2026)

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

Proof

Step	Hyp	Ref	Expression
1		ttcid	Could not format A C_ TC+ A : No typesetting found for |- A C_ TC+ A with typecode |-
2		ssexg	Could not format ( ( A C_ TC+ A /\ TC+ A e. V ) -> A e. _V ) : No typesetting found for |- ( ( A C_ TC+ A /\ TC+ A e. V ) -> A e. _V ) with typecode |-
3	1 2	mpan	Could not format ( TC+ A e. V -> A e. _V ) : No typesetting found for |- ( TC+ A e. V -> A e. _V ) with typecode |-