Theorem csbttc

Description: Distribute proper substitution through a transitive closure. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	csbttc	⊢ ⦋ 𝐴 / 𝑥 ⦌ TC+ 𝐵 = TC+ ⦋ 𝐴 / 𝑥 ⦌ 𝐵

Proof

Step	Hyp	Ref	Expression
1		csbeq1	⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ TC+ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ TC+ 𝐵 )
2		csbeq1	⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
3	2	ttceqd	⊢ ( 𝑦 = 𝐴 → TC+ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = TC+ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
4	1 3	eqeq12d	⊢ ( 𝑦 = 𝐴 → ( ⦋ 𝑦 / 𝑥 ⦌ TC+ 𝐵 = TC+ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ TC+ 𝐵 = TC+ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
5		vex	⊢ 𝑦 ∈ V
6		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
7	6	nfttc	⊢ Ⅎ 𝑥 TC+ ⦋ 𝑦 / 𝑥 ⦌ 𝐵
8		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
9	8	ttceqd	⊢ ( 𝑥 = 𝑦 → TC+ 𝐵 = TC+ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
10	5 7 9	csbief	⊢ ⦋ 𝑦 / 𝑥 ⦌ TC+ 𝐵 = TC+ ⦋ 𝑦 / 𝑥 ⦌ 𝐵
11	4 10	vtoclg	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ TC+ 𝐵 = TC+ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
12		csbprc	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ TC+ 𝐵 = ∅ )
13		csbprc	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ∅ )
14	13	ttceqd	⊢ ( ¬ 𝐴 ∈ V → TC+ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = TC+ ∅ )
15		ttc0	⊢ TC+ ∅ = ∅
16	14 15	eqtrdi	⊢ ( ¬ 𝐴 ∈ V → TC+ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ∅ )
17	12 16	eqtr4d	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ TC+ 𝐵 = TC+ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
18	11 17	pm2.61i	⊢ ⦋ 𝐴 / 𝑥 ⦌ TC+ 𝐵 = TC+ ⦋ 𝐴 / 𝑥 ⦌ 𝐵