Theorem csbov1g

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

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

Proof

Step	Hyp	Ref	Expression
1		csbov12g	$$⊢A\in V\to ⦋A/x⦌\left(BFC\right)=⦋A/x⦌BF⦋A/x⦌C$$
2		csbconstg	$$⊢A\in V\to ⦋A/x⦌C=C$$
3	2	oveq2d	$$⊢A\in V\to ⦋A/x⦌BF⦋A/x⦌C=⦋A/x⦌BFC$$
4	1 3	eqtrd	$$⊢A\in V\to ⦋A/x⦌\left(BFC\right)=⦋A/x⦌BFC$$