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

Proof

Step	Hyp	Ref	Expression
1		ttcsnexg	|- ( TC+ A e. _V -> TC+ { A } e. _V )
2		ttcsnssg	|- ( A e. V -> TC+ A C_ TC+ { A } )
3		ssexg	|- ( ( TC+ A C_ TC+ { A } /\ TC+ { A } e. _V ) -> TC+ A e. _V )
4	2 3	sylan	|- ( ( A e. V /\ TC+ { A } e. _V ) -> TC+ A e. _V )
5	4	ex	|- ( A e. V -> ( TC+ { A } e. _V -> TC+ A e. _V ) )
6	1 5	impbid2	|- ( A e. V -> ( TC+ A e. _V <-> TC+ { A } e. _V ) )