# 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 )`