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 ( ( 𝐴𝑉 𝑥 𝐵 ) → 𝐴 / 𝑥 𝐵 = 𝐵 )

Proof

Step Hyp Ref Expression
1 df-csb 𝐴 / 𝑥 𝐵 = { 𝑦[ 𝐴 / 𝑥 ] 𝑦𝐵 }
2 nfcr ( 𝑥 𝐵 → Ⅎ 𝑥 𝑦𝐵 )
3 sbctt ( ( 𝐴𝑉 ∧ Ⅎ 𝑥 𝑦𝐵 ) → ( [ 𝐴 / 𝑥 ] 𝑦𝐵𝑦𝐵 ) )
4 2 3 sylan2 ( ( 𝐴𝑉 𝑥 𝐵 ) → ( [ 𝐴 / 𝑥 ] 𝑦𝐵𝑦𝐵 ) )
5 4 abbi1dv ( ( 𝐴𝑉 𝑥 𝐵 ) → { 𝑦[ 𝐴 / 𝑥 ] 𝑦𝐵 } = 𝐵 )
6 1 5 eqtrid ( ( 𝐴𝑉 𝑥 𝐵 ) → 𝐴 / 𝑥 𝐵 = 𝐵 )