Theorem csbov2g

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

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

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⦌B=B$$
3	2	oveq1d	$$⊢A\in V\to ⦋A/x⦌BF⦋A/x⦌C=BF⦋A/x⦌C$$
4	1 3	eqtrd	$$⊢A\in V\to ⦋A/x⦌\left(BFC\right)=BF⦋A/x⦌C$$