Theorem csbov12g

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

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

Proof

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