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 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑥 𝐵 ) → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-csb | ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } | |
2 | nfcr | ⊢ ( Ⅎ 𝑥 𝐵 → Ⅎ 𝑥 𝑦 ∈ 𝐵 ) | |
3 | sbctt | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑥 𝑦 ∈ 𝐵 ) → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) ) | |
4 | 2 3 | sylan2 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑥 𝐵 ) → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) ) |
5 | 4 | abbi1dv | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑥 𝐵 ) → { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } = 𝐵 ) |
6 | 1 5 | eqtrid | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑥 𝐵 ) → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐵 ) |