Description: Formula-building deduction for class substitution. (Contributed by NM, 10-Nov-2005) (Revised by Mario Carneiro, 1-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | csbeq2dv.1 | ⊢ ( 𝜑 → 𝐵 = 𝐶 ) | |
Assertion | csbeq2dv | ⊢ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbeq2dv.1 | ⊢ ( 𝜑 → 𝐵 = 𝐶 ) | |
2 | 1 | eleq2d | ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ) |
3 | 2 | sbcbidv | ⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ) |
4 | 3 | abbidv | ⊢ ( 𝜑 → { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 } ) |
5 | df-csb | ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } | |
6 | df-csb | ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 } | |
7 | 4 5 6 | 3eqtr4g | ⊢ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) |