Theorem csbfv2g

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

	Ref	Expression
Assertion	csbfv2g	|- ( A e. C -> [_ A / x ]_ ( F ` B ) = ( F ` [_ A / x ]_ B ) )

Proof

Step	Hyp	Ref	Expression
1		csbfv12	|- [_ A / x ]_ ( F ` B ) = ( [_ A / x ]_ F ` [_ A / x ]_ B )
2		csbconstg	|- ( A e. C -> [_ A / x ]_ F = F )
3	2	fveq1d	|- ( A e. C -> ( [_ A / x ]_ F ` [_ A / x ]_ B ) = ( F ` [_ A / x ]_ B ) )
4	1 3	syl5eq	|- ( A e. C -> [_ A / x ]_ ( F ` B ) = ( F ` [_ A / x ]_ B ) )