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

Proof

Step	Hyp	Ref	Expression
1		ttcexrg	Could not format ( TC+ A e. V -> A e. _V ) : No typesetting found for |- ( TC+ A e. V -> A e. _V ) with typecode |-
2		ttcsng	Could not format ( A e. _V -> TC+ { A } = ( TC+ A u. { A } ) ) : No typesetting found for |- ( A e. _V -> TC+ { A } = ( TC+ A u. { A } ) ) with typecode |-
3	1 2	syl	Could not format ( TC+ A e. V -> TC+ { A } = ( TC+ A u. { A } ) ) : No typesetting found for |- ( TC+ A e. V -> TC+ { A } = ( TC+ A u. { A } ) ) with typecode |-
4		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
5		unexg	Could not format ( ( TC+ A e. V /\ { A } e. _V ) -> ( TC+ A u. { A } ) e. _V ) : No typesetting found for |- ( ( TC+ A e. V /\ { A } e. _V ) -> ( TC+ A u. { A } ) e. _V ) with typecode |-
6	4 5	mpan2	Could not format ( TC+ A e. V -> ( TC+ A u. { A } ) e. _V ) : No typesetting found for |- ( TC+ A e. V -> ( TC+ A u. { A } ) e. _V ) with typecode |-
7	3 6	eqeltrd	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 |-