Metamath Proof Explorer

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 
|- ( A e. _V <-> TC+ A e. _V )

Proof

Step Hyp Ref Expression
1 ttcexg 
 |-  ( A e. _V -> TC+ A e. _V )
2 ttcexrg 
 |-  ( TC+ A e. _V -> A e. _V )
3 1 2 impbii 
 |-  ( A e. _V <-> TC+ A e. _V )