Metamath Proof Explorer


Theorem csbtt

Description: Substitution doesn't affect a constant B (in which x is not free). (Contributed by Mario Carneiro, 14-Oct-2016)

Ref Expression
Assertion csbtt AV_xBA/xB=B

Proof

Step Hyp Ref Expression
1 df-csb A/xB=y|[˙A/x]˙yB
2 nfcr _xBxyB
3 sbctt AVxyB[˙A/x]˙yByB
4 2 3 sylan2 AV_xB[˙A/x]˙yByB
5 4 eqabcdv AV_xBy|[˙A/x]˙yB=B
6 1 5 eqtrid AV_xBA/xB=B