This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( 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 )