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	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 )