Theorem csbov2g

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

	Ref	Expression
Assertion	csbov2g	|- ( A e. V -> [_ A / x ]_ ( B F C ) = ( B F [_ A / x ]_ 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 ]_ B = B )
3	2	oveq1d	|- ( A e. V -> ( [_ A / x ]_ B F [_ A / x ]_ C ) = ( B F [_ A / x ]_ C ) )
4	1 3	eqtrd	|- ( A e. V -> [_ A / x ]_ ( B F C ) = ( B F [_ A / x ]_ C ) )