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

Metamath Proof Explorer

Theorem difdifdir

Description: Distributive law for class difference. Exercise 4.8 of Stoll p. 16. (Contributed by NM, 18-Aug-2004)

Ref Expression
Assertion difdifdir 
|- ( ( A \ B ) \ C ) = ( ( A \ C ) \ ( B \ C ) )

Proof

Step Hyp Ref Expression
1 dif32 
 |-  ( ( A \ B ) \ C ) = ( ( A \ C ) \ B )
2 invdif 
 |-  ( ( A \ C ) i^i ( _V \ B ) ) = ( ( A \ C ) \ B )
3 1 2 eqtr4i 
 |-  ( ( A \ B ) \ C ) = ( ( A \ C ) i^i ( _V \ B ) )
4 un0 
 |-  ( ( ( A \ C ) i^i ( _V \ B ) ) u. (/) ) = ( ( A \ C ) i^i ( _V \ B ) )
5 3 4 eqtr4i 
 |-  ( ( A \ B ) \ C ) = ( ( ( A \ C ) i^i ( _V \ B ) ) u. (/) )
6 indi 
 |-  ( ( A \ C ) i^i ( ( _V \ B ) u. C ) ) = ( ( ( A \ C ) i^i ( _V \ B ) ) u. ( ( A \ C ) i^i C ) )
7 disjdif 
 |-  ( C i^i ( A \ C ) ) = (/)
8 incom 
 |-  ( C i^i ( A \ C ) ) = ( ( A \ C ) i^i C )
9 7 8 eqtr3i 
 |-  (/) = ( ( A \ C ) i^i C )
10 9 uneq2i 
 |-  ( ( ( A \ C ) i^i ( _V \ B ) ) u. (/) ) = ( ( ( A \ C ) i^i ( _V \ B ) ) u. ( ( A \ C ) i^i C ) )
11 6 10 eqtr4i 
 |-  ( ( A \ C ) i^i ( ( _V \ B ) u. C ) ) = ( ( ( A \ C ) i^i ( _V \ B ) ) u. (/) )
12 5 11 eqtr4i 
 |-  ( ( A \ B ) \ C ) = ( ( A \ C ) i^i ( ( _V \ B ) u. C ) )
13 ddif 
 |-  ( _V \ ( _V \ C ) ) = C
14 13 uneq2i 
 |-  ( ( _V \ B ) u. ( _V \ ( _V \ C ) ) ) = ( ( _V \ B ) u. C )
15 indm 
 |-  ( _V \ ( B i^i ( _V \ C ) ) ) = ( ( _V \ B ) u. ( _V \ ( _V \ C ) ) )
16 invdif 
 |-  ( B i^i ( _V \ C ) ) = ( B \ C )
17 16 difeq2i 
 |-  ( _V \ ( B i^i ( _V \ C ) ) ) = ( _V \ ( B \ C ) )
18 15 17 eqtr3i 
 |-  ( ( _V \ B ) u. ( _V \ ( _V \ C ) ) ) = ( _V \ ( B \ C ) )
19 14 18 eqtr3i 
 |-  ( ( _V \ B ) u. C ) = ( _V \ ( B \ C ) )
20 19 ineq2i 
 |-  ( ( A \ C ) i^i ( ( _V \ B ) u. C ) ) = ( ( A \ C ) i^i ( _V \ ( B \ C ) ) )
21 invdif 
 |-  ( ( A \ C ) i^i ( _V \ ( B \ C ) ) ) = ( ( A \ C ) \ ( B \ C ) )
22 12 20 21 3eqtri 
 |-  ( ( A \ B ) \ C ) = ( ( A \ C ) \ ( B \ C ) )