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	Could not format assertion : No typesetting found for |- ( A e. V -> ( TC+ A e. _V <-> TC+ { A } e. _V ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ttcsnexg	Could not format ( TC+ A e. _V -> TC+ { A } e. _V ) : No typesetting found for |- ( TC+ A e. _V -> TC+ { A } e. _V ) with typecode |-
2		ttcsnssg	Could not format ( A e. V -> TC+ A C_ TC+ { A } ) : No typesetting found for |- ( A e. V -> TC+ A C_ TC+ { A } ) with typecode |-
3		ssexg	Could not format ( ( TC+ A C_ TC+ { A } /\ TC+ { A } e. _V ) -> TC+ A e. _V ) : No typesetting found for |- ( ( TC+ A C_ TC+ { A } /\ TC+ { A } e. _V ) -> TC+ A e. _V ) with typecode |-
4	2 3	sylan	Could not format ( ( A e. V /\ TC+ { A } e. _V ) -> TC+ A e. _V ) : No typesetting found for |- ( ( A e. V /\ TC+ { A } e. _V ) -> TC+ A e. _V ) with typecode |-
5	4	ex	Could not format ( A e. V -> ( TC+ { A } e. _V -> TC+ A e. _V ) ) : No typesetting found for |- ( A e. V -> ( TC+ { A } e. _V -> TC+ A e. _V ) ) with typecode |-
6	1 5	impbid2	Could not format ( A e. V -> ( TC+ A e. _V <-> TC+ { A } e. _V ) ) : No typesetting found for |- ( A e. V -> ( TC+ A e. _V <-> TC+ { A } e. _V ) ) with typecode |-