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	|- F/_ x A
	csbhypf.2	|- F/_ x C
	csbhypf.3	|- ( x = A -> B = C )
Assertion	csbhypf	|- ( y = A -> [_ y / x ]_ B = C )

Proof

Step	Hyp	Ref	Expression
1		csbhypf.1	|- F/_ x A
2		csbhypf.2	|- F/_ x C
3		csbhypf.3	|- ( x = A -> B = C )
4	1	nfeq2	|- F/ x y = A
5		nfcsb1v	|- F/_ x [_ y / x ]_ B
6	5 2	nfeq	|- F/ x [_ y / x ]_ B = C
7	4 6	nfim	|- F/ x ( y = A -> [_ y / x ]_ B = C )
8		eqeq1	|- ( x = y -> ( x = A <-> y = A ) )
9		csbeq1a	|- ( x = y -> B = [_ y / x ]_ B )
10	9	eqeq1d	|- ( x = y -> ( B = C <-> [_ y / x ]_ B = C ) )
11	8 10	imbi12d	|- ( x = y -> ( ( x = A -> B = C ) <-> ( y = A -> [_ y / x ]_ B = C ) ) )
12	7 11 3	chvarfv	|- ( y = A -> [_ y / x ]_ B = C )