Theorem csbov12g

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

	Ref	Expression
Assertion	csbov12g	$$⊢A\in V\to ⦋A/x⦌\left(BFC\right)=⦋A/x⦌BF⦋A/x⦌C$$

Proof

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