Theorem csbfv2g

Description: Move class substitution in and out of a function value. (Contributed by NM, 10-Nov-2005)

	Ref	Expression
Assertion	csbfv2g	$$⊢A\in C\to ⦋A/x⦌F\left(B\right)=F\left(⦋A/x⦌B\right)$$

Proof

Step	Hyp	Ref	Expression
1		csbfv12	$$⊢⦋A/x⦌F\left(B\right)=⦋A/x⦌F\left(⦋A/x⦌B\right)$$
2		csbconstg	$$⊢A\in C\to ⦋A/x⦌F=F$$
3	2	fveq1d	$$⊢A\in C\to ⦋A/x⦌F\left(⦋A/x⦌B\right)=F\left(⦋A/x⦌B\right)$$
4	1 3	syl5eq	$$⊢A\in C\to ⦋A/x⦌F\left(B\right)=F\left(⦋A/x⦌B\right)$$