Description: Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on A . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvcsbw when possible. (Contributed by Jeff Hankins, 13-Sep-2009) (Revised by Mario Carneiro, 11-Dec-2016) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbvcsb.1 | ⊢ Ⅎ 𝑦 𝐶 | |
| cbvcsb.2 | ⊢ Ⅎ 𝑥 𝐷 | ||
| cbvcsb.3 | ⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 ) | ||
| Assertion | cbvcsb | ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑦 ⦌ 𝐷 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvcsb.1 | ⊢ Ⅎ 𝑦 𝐶 | |
| 2 | cbvcsb.2 | ⊢ Ⅎ 𝑥 𝐷 | |
| 3 | cbvcsb.3 | ⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 ) | |
| 4 | 1 | nfcri | ⊢ Ⅎ 𝑦 𝑧 ∈ 𝐶 |
| 5 | 2 | nfcri | ⊢ Ⅎ 𝑥 𝑧 ∈ 𝐷 |
| 6 | 3 | eleq2d | ⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝐶 ↔ 𝑧 ∈ 𝐷 ) ) |
| 7 | 4 5 6 | cbvsbc | ⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐶 ↔ [ 𝐴 / 𝑦 ] 𝑧 ∈ 𝐷 ) |
| 8 | 7 | abbii | ⊢ { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐶 } = { 𝑧 ∣ [ 𝐴 / 𝑦 ] 𝑧 ∈ 𝐷 } |
| 9 | df-csb | ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐶 } | |
| 10 | df-csb | ⊢ ⦋ 𝐴 / 𝑦 ⦌ 𝐷 = { 𝑧 ∣ [ 𝐴 / 𝑦 ] 𝑧 ∈ 𝐷 } | |
| 11 | 8 9 10 | 3eqtr4i | ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑦 ⦌ 𝐷 |