Metamath Proof Explorer

Theorem csbin

Description: Distribute proper substitution into a class through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012) (Revised by NM, 18-Aug-2018)

Ref Expression
Assertion csbin 
|- [_ A / x ]_ ( B i^i C ) = ( [_ A / x ]_ B i^i [_ A / x ]_ C )

Proof

Step Hyp Ref Expression
1 csbeq1 
 |-  ( y = A -> [_ y / x ]_ ( B i^i C ) = [_ A / x ]_ ( B i^i C ) )
2 csbeq1 
 |-  ( y = A -> [_ y / x ]_ B = [_ A / x ]_ B )
3 csbeq1 
 |-  ( y = A -> [_ y / x ]_ C = [_ A / x ]_ C )
4 2 3 ineq12d 
 |-  ( y = A -> ( [_ y / x ]_ B i^i [_ y / x ]_ C ) = ( [_ A / x ]_ B i^i [_ A / x ]_ C ) )
5 1 4 eqeq12d 
 |-  ( y = A -> ( [_ y / x ]_ ( B i^i C ) = ( [_ y / x ]_ B i^i [_ y / x ]_ C ) <-> [_ A / x ]_ ( B i^i C ) = ( [_ A / x ]_ B i^i [_ A / x ]_ C ) ) )
6 vex 
 |-  y e. _V
7 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
8 nfcsb1v 
 |-  F/_ x [_ y / x ]_ C
9 7 8 nfin 
 |-  F/_ x ( [_ y / x ]_ B i^i [_ y / x ]_ C )
10 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
11 csbeq1a 
 |-  ( x = y -> C = [_ y / x ]_ C )
12 10 11 ineq12d 
 |-  ( x = y -> ( B i^i C ) = ( [_ y / x ]_ B i^i [_ y / x ]_ C ) )
13 6 9 12 csbief 
 |-  [_ y / x ]_ ( B i^i C ) = ( [_ y / x ]_ B i^i [_ y / x ]_ C )
14 5 13 vtoclg 
 |-  ( A e. _V -> [_ A / x ]_ ( B i^i C ) = ( [_ A / x ]_ B i^i [_ A / x ]_ C ) )
15 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ ( B i^i C ) = (/) )
16 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ B = (/) )
17 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ C = (/) )
18 16 17 ineq12d 
 |-  ( -. A e. _V -> ( [_ A / x ]_ B i^i [_ A / x ]_ C ) = ( (/) i^i (/) ) )
19 in0 
 |-  ( (/) i^i (/) ) = (/)
20 18 19 eqtr2di 
 |-  ( -. A e. _V -> (/) = ( [_ A / x ]_ B i^i [_ A / x ]_ C ) )
21 15 20 eqtrd 
 |-  ( -. A e. _V -> [_ A / x ]_ ( B i^i C ) = ( [_ A / x ]_ B i^i [_ A / x ]_ C ) )
22 14 21 pm2.61i 
 |-  [_ A / x ]_ ( B i^i C ) = ( [_ A / x ]_ B i^i [_ A / x ]_ C )