Theorem ttcsng

Description: Relationship between TC+ { A } and TC+ A : the former contains the additional element A . (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcsng	Could not format assertion : No typesetting found for |- ( A e. V -> TC+ { A } = ( TC+ A u. { A } ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ttciunun	Could not format TC+ { A } = ( U_ x e. { A } TC+ x u. { A } ) : No typesetting found for |- TC+ { A } = ( U_ x e. { A } TC+ x u. { A } ) with typecode |-
2		ttceq	Could not format ( x = A -> TC+ x = TC+ A ) : No typesetting found for |- ( x = A -> TC+ x = TC+ A ) with typecode |-
3	2	iunxsng	Could not format ( A e. V -> U_ x e. { A } TC+ x = TC+ A ) : No typesetting found for |- ( A e. V -> U_ x e. { A } TC+ x = TC+ A ) with typecode |-
4	3	uneq1d	Could not format ( A e. V -> ( U_ x e. { A } TC+ x u. { A } ) = ( TC+ A u. { A } ) ) : No typesetting found for |- ( A e. V -> ( U_ x e. { A } TC+ x u. { A } ) = ( TC+ A u. { A } ) ) with typecode |-
5	1 4	eqtrid	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 |-