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 ]_ ( B |` C ) = ( [_ A / x ]_ B |` [_ A / x ]_ C )

Proof

Step	Hyp	Ref	Expression
1		df-res	|- ( B |` C ) = ( B i^i ( C X. _V ) )
2	1	csbeq2i	|- [_ A / x ]_ ( B |` C ) = [_ A / x ]_ ( B i^i ( C X. _V ) )
3		csbxp	|- [_ A / x ]_ ( C X. _V ) = ( [_ A / x ]_ C X. [_ A / x ]_ _V )
4		csbconstg	|- ( A e. _V -> [_ A / x ]_ _V = _V )
5	4	xpeq2d	|- ( A e. _V -> ( [_ A / x ]_ C X. [_ A / x ]_ _V ) = ( [_ A / x ]_ C X. _V ) )
6	3 5	syl5eq	|- ( A e. _V -> [_ A / x ]_ ( C X. _V ) = ( [_ A / x ]_ C X. _V ) )
7		0xp	|- ( (/) X. _V ) = (/)
8	7	a1i	|- ( -. A e. _V -> ( (/) X. _V ) = (/) )
9		csbprc	|- ( -. A e. _V -> [_ A / x ]_ C = (/) )
10	9	xpeq1d	|- ( -. A e. _V -> ( [_ A / x ]_ C X. _V ) = ( (/) X. _V ) )
11		csbprc	|- ( -. A e. _V -> [_ A / x ]_ ( C X. _V ) = (/) )
12	8 10 11	3eqtr4rd	|- ( -. A e. _V -> [_ A / x ]_ ( C X. _V ) = ( [_ A / x ]_ C X. _V ) )
13	6 12	pm2.61i	|- [_ A / x ]_ ( C X. _V ) = ( [_ A / x ]_ C X. _V )
14	13	ineq2i	|- ( [_ A / x ]_ B i^i [_ A / x ]_ ( C X. _V ) ) = ( [_ A / x ]_ B i^i ( [_ A / x ]_ C X. _V ) )
15		csbin	|- [_ A / x ]_ ( B i^i ( C X. _V ) ) = ( [_ A / x ]_ B i^i [_ A / x ]_ ( C X. _V ) )
16		df-res	|- ( [_ A / x ]_ B |` [_ A / x ]_ C ) = ( [_ A / x ]_ B i^i ( [_ A / x ]_ C X. _V ) )
17	14 15 16	3eqtr4i	|- [_ A / x ]_ ( B i^i ( C X. _V ) ) = ( [_ A / x ]_ B |` [_ A / x ]_ C )
18	2 17	eqtri	|- [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B |` [_ A / x ]_ C )