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	eqabcdv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑥 𝐵 ) → { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } = 𝐵 )
6	1 5	eqtrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑥 𝐵 ) → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐵 )