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	$$⊢\underset{\_}{Ⅎ}xA$$
	csbhypf.2	$$⊢\underset{\_}{Ⅎ}xC$$
	csbhypf.3	$$⊢x=A\to B=C$$
Assertion	csbhypf	$$⊢y=A\to ⦋y/x⦌B=C$$

Proof

Step	Hyp	Ref	Expression
1		csbhypf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		csbhypf.2	$$⊢\underset{\_}{Ⅎ}xC$$
3		csbhypf.3	$$⊢x=A\to B=C$$
4	1	nfeq2	$$⊢Ⅎxy=A$$
5		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
6	5 2	nfeq	$$⊢Ⅎx⦋y/x⦌B=C$$
7	4 6	nfim	$$⊢Ⅎx\left(y=A\to ⦋y/x⦌B=C\right)$$
8		eqeq1	$$⊢x=y\to \left(x=A\leftrightarrow y=A\right)$$
9		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
10	9	eqeq1d	$$⊢x=y\to \left(B=C\leftrightarrow ⦋y/x⦌B=C\right)$$
11	8 10	imbi12d	$$⊢x=y\to \left(\left(x=A\to B=C\right)\leftrightarrow \left(y=A\to ⦋y/x⦌B=C\right)\right)$$
12	7 11 3	chvarfv	$$⊢y=A\to ⦋y/x⦌B=C$$