Theorem csbov123

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

	Ref	Expression
Assertion	csbov123	$$⊢⦋A/x⦌\left(BFC\right)=⦋A/x⦌B⦋A/x⦌F⦋A/x⦌C$$

Proof

Step	Hyp	Ref	Expression
1		csbeq1	$$⊢y=A\to ⦋y/x⦌\left(BFC\right)=⦋A/x⦌\left(BFC\right)$$
2		csbeq1	$$⊢y=A\to ⦋y/x⦌F=⦋A/x⦌F$$
3		csbeq1	$$⊢y=A\to ⦋y/x⦌B=⦋A/x⦌B$$
4		csbeq1	$$⊢y=A\to ⦋y/x⦌C=⦋A/x⦌C$$
5	2 3 4	oveq123d	$$⊢y=A\to ⦋y/x⦌B⦋y/x⦌F⦋y/x⦌C=⦋A/x⦌B⦋A/x⦌F⦋A/x⦌C$$
6	1 5	eqeq12d	$$⊢y=A\to \left(⦋y/x⦌\left(BFC\right)=⦋y/x⦌B⦋y/x⦌F⦋y/x⦌C\leftrightarrow ⦋A/x⦌\left(BFC\right)=⦋A/x⦌B⦋A/x⦌F⦋A/x⦌C\right)$$
7		vex	$$⊢y\in \mathrm{V}$$
8		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
9		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌F$$
10		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌C$$
11	8 9 10	nfov	$$⊢\underset{\_}{Ⅎ}x\left(⦋y/x⦌B⦋y/x⦌F⦋y/x⦌C\right)$$
12		csbeq1a	$$⊢x=y\to F=⦋y/x⦌F$$
13		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
14		csbeq1a	$$⊢x=y\to C=⦋y/x⦌C$$
15	12 13 14	oveq123d	$$⊢x=y\to BFC=⦋y/x⦌B⦋y/x⦌F⦋y/x⦌C$$
16	7 11 15	csbief	$$⊢⦋y/x⦌\left(BFC\right)=⦋y/x⦌B⦋y/x⦌F⦋y/x⦌C$$
17	6 16	vtoclg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌\left(BFC\right)=⦋A/x⦌B⦋A/x⦌F⦋A/x⦌C$$
18		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌\left(BFC\right)=\varnothing$$
19		df-ov	$$⊢⦋A/x⦌B⦋A/x⦌F⦋A/x⦌C=⦋A/x⦌F\left(⟨⦋A/x⦌B,⦋A/x⦌C⟩\right)$$
20		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌F=\varnothing$$
21	20	fveq1d	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌F\left(⟨⦋A/x⦌B,⦋A/x⦌C⟩\right)=\varnothing \left(⟨⦋A/x⦌B,⦋A/x⦌C⟩\right)$$
22		0fv	$$⊢\varnothing \left(⟨⦋A/x⦌B,⦋A/x⦌C⟩\right)=\varnothing$$
23	21 22	eqtrdi	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌F\left(⟨⦋A/x⦌B,⦋A/x⦌C⟩\right)=\varnothing$$
24	19 23	syl5req	$$⊢\neg A\in \mathrm{V}\to \varnothing =⦋A/x⦌B⦋A/x⦌F⦋A/x⦌C$$
25	18 24	eqtrd	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌\left(BFC\right)=⦋A/x⦌B⦋A/x⦌F⦋A/x⦌C$$
26	17 25	pm2.61i	$$⊢⦋A/x⦌\left(BFC\right)=⦋A/x⦌B⦋A/x⦌F⦋A/x⦌C$$