Metamath Proof Explorer

Theorem csbttc

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

Ref Expression
Assertion csbttc 
|- [_ A / x ]_ TC+ B = TC+ [_ A / x ]_ B

Proof

Step Hyp Ref Expression
1 csbeq1 
 |-  ( y = A -> [_ y / x ]_ TC+ B = [_ A / x ]_ TC+ B )
2 csbeq1 
 |-  ( y = A -> [_ y / x ]_ B = [_ A / x ]_ B )
3 2 ttceqd 
 |-  ( y = A -> TC+ [_ y / x ]_ B = TC+ [_ A / x ]_ B )
4 1 3 eqeq12d 
 |-  ( y = A -> ( [_ y / x ]_ TC+ B = TC+ [_ y / x ]_ B <-> [_ A / x ]_ TC+ B = TC+ [_ A / x ]_ B ) )
5 vex 
 |-  y e. _V
6 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
7 6 nfttc 
 |-  F/_ x TC+ [_ y / x ]_ B
8 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
9 8 ttceqd 
 |-  ( x = y -> TC+ B = TC+ [_ y / x ]_ B )
10 5 7 9 csbief 
 |-  [_ y / x ]_ TC+ B = TC+ [_ y / x ]_ B
11 4 10 vtoclg 
 |-  ( A e. _V -> [_ A / x ]_ TC+ B = TC+ [_ A / x ]_ B )
12 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ TC+ B = (/) )
13 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ B = (/) )
14 13 ttceqd 
 |-  ( -. A e. _V -> TC+ [_ A / x ]_ B = TC+ (/) )
15 ttc0 
 |-  TC+ (/) = (/)
16 14 15 eqtrdi 
 |-  ( -. A e. _V -> TC+ [_ A / x ]_ B = (/) )
17 12 16 eqtr4d 
 |-  ( -. A e. _V -> [_ A / x ]_ TC+ B = TC+ [_ A / x ]_ B )
18 11 17 pm2.61i 
 |-  [_ A / x ]_ TC+ B = TC+ [_ A / x ]_ B