Theorem csbaovg

Description: Move class substitution in and out of an operation. (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Assertion	csbaovg	$$⊢A\in D\to ⦋A/x⦌((BFC))=((⦋A/x⦌B⦋A/x⦌F⦋A/x⦌C))$$

Proof

Step	Hyp	Ref	Expression
1		csbeq1	$$⊢y=A\to ⦋y/x⦌((BFC))=⦋A/x⦌((BFC))$$
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	aoveq123d	$$⊢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⦌((BFC))=((⦋y/x⦌B⦋y/x⦌F⦋y/x⦌C))\leftrightarrow ⦋A/x⦌((BFC))=((⦋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	nfaov	$$⊢\underset{\_}{Ⅎ}x((⦋y/x⦌B⦋y/x⦌F⦋y/x⦌C))$$
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	aoveq123d	$$⊢x=y\to ((BFC))=((⦋y/x⦌B⦋y/x⦌F⦋y/x⦌C))$$
16	7 11 15	csbief	$$⊢⦋y/x⦌((BFC))=((⦋y/x⦌B⦋y/x⦌F⦋y/x⦌C))$$
17	6 16	vtoclg	$$⊢A\in D\to ⦋A/x⦌((BFC))=((⦋A/x⦌B⦋A/x⦌F⦋A/x⦌C))$$