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

Metamath Proof Explorer

Theorem csbdif

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

Ref Expression
Assertion csbdif 
|- [_ A / x ]_ ( B \ C ) = ( [_ A / x ]_ B \ [_ A / x ]_ C )

Proof

Step Hyp Ref Expression
1 csbeq1 
 |-  ( y = A -> [_ y / x ]_ ( B \ C ) = [_ A / x ]_ ( B \ C ) )
2 csbeq1 
 |-  ( y = A -> [_ y / x ]_ B = [_ A / x ]_ B )
3 csbeq1 
 |-  ( y = A -> [_ y / x ]_ C = [_ A / x ]_ C )
4 2 3 difeq12d 
 |-  ( y = A -> ( [_ y / x ]_ B \ [_ y / x ]_ C ) = ( [_ A / x ]_ B \ [_ A / x ]_ C ) )
5 1 4 eqeq12d 
 |-  ( y = A -> ( [_ y / x ]_ ( B \ C ) = ( [_ y / x ]_ B \ [_ y / x ]_ C ) <-> [_ A / x ]_ ( B \ C ) = ( [_ A / x ]_ B \ [_ 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 nfdif 
 |-  F/_ x ( [_ y / x ]_ B \ [_ y / x ]_ C )
10 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
11 csbeq1a 
 |-  ( x = y -> C = [_ y / x ]_ C )
12 10 11 difeq12d 
 |-  ( x = y -> ( B \ C ) = ( [_ y / x ]_ B \ [_ y / x ]_ C ) )
13 6 9 12 csbief 
 |-  [_ y / x ]_ ( B \ C ) = ( [_ y / x ]_ B \ [_ y / x ]_ C )
14 5 13 vtoclg 
 |-  ( A e. _V -> [_ A / x ]_ ( B \ C ) = ( [_ A / x ]_ B \ [_ A / x ]_ C ) )
15 dif0 
 |-  ( (/) \ (/) ) = (/)
16 15 a1i 
 |-  ( -. A e. _V -> ( (/) \ (/) ) = (/) )
17 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ B = (/) )
18 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ C = (/) )
19 17 18 difeq12d 
 |-  ( -. A e. _V -> ( [_ A / x ]_ B \ [_ A / x ]_ C ) = ( (/) \ (/) ) )
20 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ ( B \ C ) = (/) )
21 16 19 20 3eqtr4rd 
 |-  ( -. A e. _V -> [_ A / x ]_ ( B \ C ) = ( [_ A / x ]_ B \ [_ A / x ]_ C ) )
22 14 21 pm2.61i 
 |-  [_ A / x ]_ ( B \ C ) = ( [_ A / x ]_ B \ [_ A / x ]_ C )