Theorem csbres

Description: Distribute proper substitution through the restriction of a class. (Contributed by Alan Sare, 10-Nov-2012) (Revised by NM, 23-Aug-2018)

	Ref	Expression
Assertion	csbres	$$⊢⦋A/x⦌\left({B\upharpoonright }_C\right)={⦋A/x⦌B\upharpoonright }_{⦋A/x⦌C}$$

Proof

Step	Hyp	Ref	Expression
1		df-res	$$⊢{B\upharpoonright }_C=B\cap \left(C\times \mathrm{V}\right)$$
2	1	csbeq2i	$$⊢⦋A/x⦌\left({B\upharpoonright }_C\right)=⦋A/x⦌\left(B\cap \left(C\times \mathrm{V}\right)\right)$$
3		csbxp	$$⊢⦋A/x⦌\left(C\times \mathrm{V}\right)=⦋A/x⦌C\times ⦋A/x⦌\mathrm{V}$$
4		csbconstg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌\mathrm{V}=\mathrm{V}$$
5	4	xpeq2d	$$⊢A\in \mathrm{V}\to ⦋A/x⦌C\times ⦋A/x⦌\mathrm{V}=⦋A/x⦌C\times \mathrm{V}$$
6	3 5	syl5eq	$$⊢A\in \mathrm{V}\to ⦋A/x⦌\left(C\times \mathrm{V}\right)=⦋A/x⦌C\times \mathrm{V}$$
7		0xp	$$⊢\varnothing \times \mathrm{V}=\varnothing$$
8	7	a1i	$$⊢\neg A\in \mathrm{V}\to \varnothing \times \mathrm{V}=\varnothing$$
9		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌C=\varnothing$$
10	9	xpeq1d	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌C\times \mathrm{V}=\varnothing \times \mathrm{V}$$
11		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌\left(C\times \mathrm{V}\right)=\varnothing$$
12	8 10 11	3eqtr4rd	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌\left(C\times \mathrm{V}\right)=⦋A/x⦌C\times \mathrm{V}$$
13	6 12	pm2.61i	$$⊢⦋A/x⦌\left(C\times \mathrm{V}\right)=⦋A/x⦌C\times \mathrm{V}$$
14	13	ineq2i	$$⊢⦋A/x⦌B\cap ⦋A/x⦌\left(C\times \mathrm{V}\right)=⦋A/x⦌B\cap \left(⦋A/x⦌C\times \mathrm{V}\right)$$
15		csbin	$$⊢⦋A/x⦌\left(B\cap \left(C\times \mathrm{V}\right)\right)=⦋A/x⦌B\cap ⦋A/x⦌\left(C\times \mathrm{V}\right)$$
16		df-res	$$⊢{⦋A/x⦌B\upharpoonright }_{⦋A/x⦌C}=⦋A/x⦌B\cap \left(⦋A/x⦌C\times \mathrm{V}\right)$$
17	14 15 16	3eqtr4i	$$⊢⦋A/x⦌\left(B\cap \left(C\times \mathrm{V}\right)\right)={⦋A/x⦌B\upharpoonright }_{⦋A/x⦌C}$$
18	2 17	eqtri	$$⊢⦋A/x⦌\left({B\upharpoonright }_C\right)={⦋A/x⦌B\upharpoonright }_{⦋A/x⦌C}$$