Theorem csbiedf

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

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

Proof

Step	Hyp	Ref	Expression
1		csbiedf.1	⊢ Ⅎ 𝑥 𝜑
2		csbiedf.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐶 )
3		csbiedf.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		csbiedf.4	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 = 𝐶 )
5	4	ex	⊢ ( 𝜑 → ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) )
6	1 5	alrimi	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) )
7		csbiebt	⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑥 𝐶 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 ) )
8	3 2 7	syl2anc	⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 ) )
9	6 8	mpbid	⊢ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 )