Theorem ttceq

Description: Equality theorem for transitive closure. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttceq	Could not format assertion : No typesetting found for |- ( A = B -> TC+ A = TC+ B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		iuneq1	$$⊢A=B\to \bigcup _{x\in A}\bigcup \mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),\left\{x\right\}\right)\left[\mathrm{\omega }\right]=\bigcup _{x\in B}\bigcup \mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),\left\{x\right\}\right)\left[\mathrm{\omega }\right]$$
2		df-ttc	Could not format TC+ A = U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) : No typesetting found for |- TC+ A = U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) with typecode |-
3		df-ttc	Could not format TC+ B = U_ x e. B U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) : No typesetting found for |- TC+ B = U_ x e. B U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) with typecode |-
4	1 2 3	3eqtr4g	Could not format ( A = B -> TC+ A = TC+ B ) : No typesetting found for |- ( A = B -> TC+ A = TC+ B ) with typecode |-