Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019) Reduce axiom usage. (Revised by GG, 15-Oct-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | csbie.1 | ⊢ 𝐴 ∈ V | |
csbie.2 | ⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) | ||
Assertion | csbie | ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbie.1 | ⊢ 𝐴 ∈ V | |
2 | csbie.2 | ⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) | |
3 | df-csb | ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } | |
4 | 2 | eleq2d | ⊢ ( 𝑥 = 𝐴 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ) |
5 | 1 4 | sbcie | ⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) |
6 | 5 | abbii | ⊢ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } = { 𝑦 ∣ 𝑦 ∈ 𝐶 } |
7 | abid2 | ⊢ { 𝑦 ∣ 𝑦 ∈ 𝐶 } = 𝐶 | |
8 | 3 6 7 | 3eqtri | ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 |