Theorem ttcexbi

Description: A class is a set iff its transitive closure is a set, assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcexbi	⊢ ( 𝐴 ∈ V ↔ TC+ 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		ttcexg	⊢ ( 𝐴 ∈ V → TC+ 𝐴 ∈ V )
2		ttcexrg	⊢ ( TC+ 𝐴 ∈ V → 𝐴 ∈ V )
3	1 2	impbii	⊢ ( 𝐴 ∈ V ↔ TC+ 𝐴 ∈ V )