Theorem ttcsnexg

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

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

Proof

Step	Hyp	Ref	Expression
1		ttcexrg	⊢ ( TC+ 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2		ttcsng	⊢ ( 𝐴 ∈ V → TC+ { 𝐴 } = ( TC+ 𝐴 ∪ { 𝐴 } ) )
3	1 2	syl	⊢ ( TC+ 𝐴 ∈ 𝑉 → TC+ { 𝐴 } = ( TC+ 𝐴 ∪ { 𝐴 } ) )
4		snex	⊢ { 𝐴 } ∈ V
5		unexg	⊢ ( ( TC+ 𝐴 ∈ 𝑉 ∧ { 𝐴 } ∈ V ) → ( TC+ 𝐴 ∪ { 𝐴 } ) ∈ V )
6	4 5	mpan2	⊢ ( TC+ 𝐴 ∈ 𝑉 → ( TC+ 𝐴 ∪ { 𝐴 } ) ∈ V )
7	3 6	eqeltrd	⊢ ( TC+ 𝐴 ∈ 𝑉 → TC+ { 𝐴 } ∈ V )