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

Metamath Proof Explorer

Theorem csbied

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014) (Revised by Mario Carneiro, 13-Oct-2016) Reduce axiom usage. (Revised by GG, 15-Oct-2024)

Ref Expression
Hypotheses csbied.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
csbied.2 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 = 𝐶 )
Assertion csbied ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 )

Proof

Step Hyp Ref Expression
1 csbied.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 csbied.2 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 = 𝐶 )
3 df-csb ⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 }
4 2 eleq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶 ) )
5 1 4 sbcied ⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶 ) )
6 5 alrimiv ⊢ ( 𝜑 → ∀ 𝑧 ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶 ) )
7 df-clab ⊢ ( 𝑧 ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } ↔ [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 )
8 eleq1w ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵 ) )
9 8 sbcbidv ⊢ ( 𝑦 = 𝑧 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐵 ) )
10 9 sbievw ⊢ ( [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐵 )
11 7 10 bitr2i ⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } )
12 11 bibi1i ⊢ ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶 ) ↔ ( 𝑧 ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } ↔ 𝑧 ∈ 𝐶 ) )
13 12 biimpi ⊢ ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶 ) → ( 𝑧 ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } ↔ 𝑧 ∈ 𝐶 ) )
14 6 13 sylg ⊢ ( 𝜑 → ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } ↔ 𝑧 ∈ 𝐶 ) )
15 dfcleq ⊢ ( { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } = 𝐶 ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } ↔ 𝑧 ∈ 𝐶 ) )
16 14 15 sylibr ⊢ ( 𝜑 → { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 } = 𝐶 )
17 3 16 eqtrid ⊢ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 )