Theorem csbov1g

Description: Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005)

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

Proof

Step	Hyp	Ref	Expression
1		csbov12g	|- ( A e. V -> [_ A / x ]_ ( B F C ) = ( [_ A / x ]_ B F [_ A / x ]_ C ) )
2		csbconstg	|- ( A e. V -> [_ A / x ]_ C = C )
3	2	oveq2d	|- ( A e. V -> ( [_ A / x ]_ B F [_ A / x ]_ C ) = ( [_ A / x ]_ B F C ) )
4	1 3	eqtrd	|- ( A e. V -> [_ A / x ]_ ( B F C ) = ( [_ A / x ]_ B F C ) )