Description: Change the bound variable of a proper substitution into a class using implicit substitution. (Contributed by NM, 30-Sep-2008) (Revised by Mario Carneiro, 13-Oct-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cbvcsbv.1 | ⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 ) | |
| Assertion | cbvcsbv | ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑦 ⦌ 𝐶 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvcsbv.1 | ⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 ) | |
| 2 | 1 | eleq2d | ⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶 ) ) |
| 3 | 2 | cbvsbcvw | ⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐵 ↔ [ 𝐴 / 𝑦 ] 𝑧 ∈ 𝐶 ) |
| 4 | 3 | abbii | ⊢ { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐵 } = { 𝑧 ∣ [ 𝐴 / 𝑦 ] 𝑧 ∈ 𝐶 } |
| 5 | df-csb | ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐵 } | |
| 6 | df-csb | ⊢ ⦋ 𝐴 / 𝑦 ⦌ 𝐶 = { 𝑧 ∣ [ 𝐴 / 𝑦 ] 𝑧 ∈ 𝐶 } | |
| 7 | 4 5 6 | 3eqtr4i | ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑦 ⦌ 𝐶 |