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	⊢ ( TC+ 𝐴 ∈ 𝑉 → 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		ttcid	⊢ 𝐴 ⊆ TC+ 𝐴
2		ssexg	⊢ ( ( 𝐴 ⊆ TC+ 𝐴 ∧ TC+ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ V )
3	1 2	mpan	⊢ ( TC+ 𝐴 ∈ 𝑉 → 𝐴 ∈ V )