Theorem csbttc

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

	Ref	Expression
Assertion	csbttc	Could not format assertion : No typesetting found for |- [_ A / x ]_ TC+ B = TC+ [_ A / x ]_ B with typecode |-

Proof

Step	Hyp	Ref	Expression
1		csbeq1	Could not format ( y = A -> [_ y / x ]_ TC+ B = [_ A / x ]_ TC+ B ) : No typesetting found for |- ( y = A -> [_ y / x ]_ TC+ B = [_ A / x ]_ TC+ B ) with typecode |-
2		csbeq1	$$⊢y=A\to ⦋y/x⦌B=⦋A/x⦌B$$
3	2	ttceqd	Could not format ( y = A -> TC+ [_ y / x ]_ B = TC+ [_ A / x ]_ B ) : No typesetting found for |- ( y = A -> TC+ [_ y / x ]_ B = TC+ [_ A / x ]_ B ) with typecode |-
4	1 3	eqeq12d	Could not format ( y = A -> ( [_ y / x ]_ TC+ B = TC+ [_ y / x ]_ B <-> [_ A / x ]_ TC+ B = TC+ [_ A / x ]_ B ) ) : No typesetting found for |- ( y = A -> ( [_ y / x ]_ TC+ B = TC+ [_ y / x ]_ B <-> [_ A / x ]_ TC+ B = TC+ [_ A / x ]_ B ) ) with typecode |-
5		vex	$$⊢y\in \mathrm{V}$$
6		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
7	6	nfttc	Could not format F/_ x TC+ [_ y / x ]_ B : No typesetting found for |- F/_ x TC+ [_ y / x ]_ B with typecode |-
8		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
9	8	ttceqd	Could not format ( x = y -> TC+ B = TC+ [_ y / x ]_ B ) : No typesetting found for |- ( x = y -> TC+ B = TC+ [_ y / x ]_ B ) with typecode |-
10	5 7 9	csbief	Could not format [_ y / x ]_ TC+ B = TC+ [_ y / x ]_ B : No typesetting found for |- [_ y / x ]_ TC+ B = TC+ [_ y / x ]_ B with typecode |-
11	4 10	vtoclg	Could not format ( A e. _V -> [_ A / x ]_ TC+ B = TC+ [_ A / x ]_ B ) : No typesetting found for |- ( A e. _V -> [_ A / x ]_ TC+ B = TC+ [_ A / x ]_ B ) with typecode |-
12		csbprc	Could not format ( -. A e. _V -> [_ A / x ]_ TC+ B = (/) ) : No typesetting found for |- ( -. A e. _V -> [_ A / x ]_ TC+ B = (/) ) with typecode |-
13		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B=\varnothing$$
14	13	ttceqd	Could not format ( -. A e. _V -> TC+ [_ A / x ]_ B = TC+ (/) ) : No typesetting found for |- ( -. A e. _V -> TC+ [_ A / x ]_ B = TC+ (/) ) with typecode |-
15		ttc0	Could not format TC+ (/) = (/) : No typesetting found for |- TC+ (/) = (/) with typecode |-
16	14 15	eqtrdi	Could not format ( -. A e. _V -> TC+ [_ A / x ]_ B = (/) ) : No typesetting found for |- ( -. A e. _V -> TC+ [_ A / x ]_ B = (/) ) with typecode |-
17	12 16	eqtr4d	Could not format ( -. A e. _V -> [_ A / x ]_ TC+ B = TC+ [_ A / x ]_ B ) : No typesetting found for |- ( -. A e. _V -> [_ A / x ]_ TC+ B = TC+ [_ A / x ]_ B ) with typecode |-
18	11 17	pm2.61i	Could not format [_ A / x ]_ TC+ B = TC+ [_ A / x ]_ B : No typesetting found for |- [_ A / x ]_ TC+ B = TC+ [_ A / x ]_ B with typecode |-