Theorem csbied2

Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		csbied2.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		csbied2.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
3		csbied2.3	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝐶 = 𝐷 )
4		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
5	4 2	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝑥 = 𝐵 )
6	5 3	syldan	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐶 = 𝐷 )
7	1 6	csbied	⊢ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = 𝐷 )