Theorem csbief

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

	Ref	Expression
Hypotheses	csbief.1	|- A e. _V
	csbief.2	|- F/_ x C
	csbief.3	|- ( x = A -> B = C )
Assertion	csbief	|- [_ A / x ]_ B = C

Proof

Step	Hyp	Ref	Expression
1		csbief.1	|- A e. _V
2		csbief.2	|- F/_ x C
3		csbief.3	|- ( x = A -> B = C )
4	2	a1i	|- ( A e. _V -> F/_ x C )
5	4 3	csbiegf	|- ( A e. _V -> [_ A / x ]_ B = C )
6	1 5	ax-mp	|- [_ A / x ]_ B = C