This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem csbie

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 ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶

Proof

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 ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶