Theorem ttceq

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

	Ref	Expression
Assertion	ttceq	⊢ ( 𝐴 = 𝐵 → TC+ 𝐴 = TC+ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		iuneq1	⊢ ( 𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) = ∪ 𝑥 ∈ 𝐵 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω ) )
2		df-ttc	⊢ TC+ 𝐴 = ∪ 𝑥 ∈ 𝐴 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω )
3		df-ttc	⊢ TC+ 𝐵 = ∪ 𝑥 ∈ 𝐵 ∪ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , { 𝑥 } ) “ ω )
4	1 2 3	3eqtr4g	⊢ ( 𝐴 = 𝐵 → TC+ 𝐴 = TC+ 𝐵 )