Theorem csbhypf

Description: Introduce an explicit substitution into an implicit substitution hypothesis. See sbhypf for class substitution version. (Contributed by NM, 19-Dec-2008)

	Ref	Expression
Hypotheses	csbhypf.1	⊢ Ⅎ 𝑥 𝐴
	csbhypf.2	⊢ Ⅎ 𝑥 𝐶
	csbhypf.3	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
Assertion	csbhypf	⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		csbhypf.1	⊢ Ⅎ 𝑥 𝐴
2		csbhypf.2	⊢ Ⅎ 𝑥 𝐶
3		csbhypf.3	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
4	1	nfeq2	⊢ Ⅎ 𝑥 𝑦 = 𝐴
5		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
6	5 2	nfeq	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐶
7	4 6	nfim	⊢ Ⅎ 𝑥 ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐶 )
8		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐴 ) )
9		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
10	9	eqeq1d	⊢ ( 𝑥 = 𝑦 → ( 𝐵 = 𝐶 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐶 ) )
11	8 10	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ↔ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐶 ) ) )
12	7 11 3	chvarfv	⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐶 )