Theorem ttcsnexbig

Description: The transitive closure of a set is a set iff its singleton transitive closure is a set. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcsnexbig	⊢ ( 𝐴 ∈ 𝑉 → ( TC+ 𝐴 ∈ V ↔ TC+ { 𝐴 } ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		ttcsnexg	⊢ ( TC+ 𝐴 ∈ V → TC+ { 𝐴 } ∈ V )
2		ttcsnssg	⊢ ( 𝐴 ∈ 𝑉 → TC+ 𝐴 ⊆ TC+ { 𝐴 } )
3		ssexg	⊢ ( ( TC+ 𝐴 ⊆ TC+ { 𝐴 } ∧ TC+ { 𝐴 } ∈ V ) → TC+ 𝐴 ∈ V )
4	2 3	sylan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ TC+ { 𝐴 } ∈ V ) → TC+ 𝐴 ∈ V )
5	4	ex	⊢ ( 𝐴 ∈ 𝑉 → ( TC+ { 𝐴 } ∈ V → TC+ 𝐴 ∈ V ) )
6	1 5	impbid2	⊢ ( 𝐴 ∈ 𝑉 → ( TC+ 𝐴 ∈ V ↔ TC+ { 𝐴 } ∈ V ) )