Theorem csbov

Description: Move class substitution in and out of an operation. (Contributed by NM, 23-Aug-2018)

	Ref	Expression
Assertion	csbov	$$⊢⦋A/x⦌\left(BFC\right)=B⦋A/x⦌FC$$

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 \mathrm{V}\to ⦋A/x⦌B=B$$
3		csbconstg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌C=C$$
4	2 3	oveq12d	$$⊢A\in \mathrm{V}\to ⦋A/x⦌B⦋A/x⦌F⦋A/x⦌C=B⦋A/x⦌FC$$
5		0fv	$$⊢\varnothing \left(⟨B,C⟩\right)=\varnothing$$
6		df-ov	$$⊢B\varnothing C=\varnothing \left(⟨B,C⟩\right)$$
7		0ov	$$⊢⦋A/x⦌B\varnothing ⦋A/x⦌C=\varnothing$$
8	5 6 7	3eqtr4ri	$$⊢⦋A/x⦌B\varnothing ⦋A/x⦌C=B\varnothing C$$
9		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌F=\varnothing$$
10	9	oveqd	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B⦋A/x⦌F⦋A/x⦌C=⦋A/x⦌B\varnothing ⦋A/x⦌C$$
11	9	oveqd	$$⊢\neg A\in \mathrm{V}\to B⦋A/x⦌FC=B\varnothing C$$
12	8 10 11	3eqtr4a	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B⦋A/x⦌F⦋A/x⦌C=B⦋A/x⦌FC$$
13	4 12	pm2.61i	$$⊢⦋A/x⦌B⦋A/x⦌F⦋A/x⦌C=B⦋A/x⦌FC$$
14	1 13	eqtri	$$⊢⦋A/x⦌\left(BFC\right)=B⦋A/x⦌FC$$