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

Metamath Proof Explorer

Theorem csbiegf

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 11-Nov-2005) (Revised by Mario Carneiro, 13-Oct-2016)

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

Proof

Step Hyp Ref Expression
1 csbiegf.1 ⊢ ( 𝐴 ∈ 𝑉 → Ⅎ 𝑥 𝐶 )
2 csbiegf.2 ⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
3 2 ax-gen ⊢ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
4 csbiebt ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑥 𝐶 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 ) )
5 1 4 mpdan ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 ) )
6 3 5 mpbii ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 )