Theorem ttceq

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

	Ref	Expression
Assertion	ttceq	|- ( A = B -> TC+ A = TC+ B )

Proof

Step	Hyp	Ref	Expression
1		iuneq1	|- ( A = B -> U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) = U_ x e. B U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) )
2		df-ttc	|- TC+ A = U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om )
3		df-ttc	|- TC+ B = U_ x e. B U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om )
4	1 2 3	3eqtr4g	|- ( A = B -> TC+ A = TC+ B )