Theorem csbdif

Description: Distribution of class substitution over difference of two classes. (Contributed by ML, 14-Jul-2020)

	Ref	Expression
Assertion	csbdif	$$⊢⦋A/x⦌\left(B\setminus C\right)=⦋A/x⦌B\setminus ⦋A/x⦌C$$

Proof

Step	Hyp	Ref	Expression
1		csbeq1	$$⊢y=A\to ⦋y/x⦌\left(B\setminus C\right)=⦋A/x⦌\left(B\setminus C\right)$$
2		csbeq1	$$⊢y=A\to ⦋y/x⦌B=⦋A/x⦌B$$
3		csbeq1	$$⊢y=A\to ⦋y/x⦌C=⦋A/x⦌C$$
4	2 3	difeq12d	$$⊢y=A\to ⦋y/x⦌B\setminus ⦋y/x⦌C=⦋A/x⦌B\setminus ⦋A/x⦌C$$
5	1 4	eqeq12d	$$⊢y=A\to \left(⦋y/x⦌\left(B\setminus C\right)=⦋y/x⦌B\setminus ⦋y/x⦌C\leftrightarrow ⦋A/x⦌\left(B\setminus C\right)=⦋A/x⦌B\setminus ⦋A/x⦌C\right)$$
6		vex	$$⊢y\in \mathrm{V}$$
7		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
8		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌C$$
9	7 8	nfdif	$$⊢\underset{\_}{Ⅎ}x\left(⦋y/x⦌B\setminus ⦋y/x⦌C\right)$$
10		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
11		csbeq1a	$$⊢x=y\to C=⦋y/x⦌C$$
12	10 11	difeq12d	$$⊢x=y\to B\setminus C=⦋y/x⦌B\setminus ⦋y/x⦌C$$
13	6 9 12	csbief	$$⊢⦋y/x⦌\left(B\setminus C\right)=⦋y/x⦌B\setminus ⦋y/x⦌C$$
14	5 13	vtoclg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌\left(B\setminus C\right)=⦋A/x⦌B\setminus ⦋A/x⦌C$$
15		dif0	$$⊢\varnothing \setminus \varnothing =\varnothing$$
16	15	a1i	$$⊢\neg A\in \mathrm{V}\to \varnothing \setminus \varnothing =\varnothing$$
17		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B=\varnothing$$
18		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌C=\varnothing$$
19	17 18	difeq12d	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B\setminus ⦋A/x⦌C=\varnothing \setminus \varnothing$$
20		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌\left(B\setminus C\right)=\varnothing$$
21	16 19 20	3eqtr4rd	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌\left(B\setminus C\right)=⦋A/x⦌B\setminus ⦋A/x⦌C$$
22	14 21	pm2.61i	$$⊢⦋A/x⦌\left(B\setminus C\right)=⦋A/x⦌B\setminus ⦋A/x⦌C$$