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

Metamath Proof Explorer

Theorem difundi

Description: Distributive law for class difference. Theorem 39 of Suppes p. 29. (Contributed by NM, 17-Aug-2004)

Ref Expression
Assertion difundi 
|- ( A \ ( B u. C ) ) = ( ( A \ B ) i^i ( A \ C ) )

Proof

Step Hyp Ref Expression
1 dfun3 
 |-  ( B u. C ) = ( _V \ ( ( _V \ B ) i^i ( _V \ C ) ) )
2 1 difeq2i 
 |-  ( A \ ( B u. C ) ) = ( A \ ( _V \ ( ( _V \ B ) i^i ( _V \ C ) ) ) )
3 inindi 
 |-  ( A i^i ( ( _V \ B ) i^i ( _V \ C ) ) ) = ( ( A i^i ( _V \ B ) ) i^i ( A i^i ( _V \ C ) ) )
4 dfin2 
 |-  ( A i^i ( ( _V \ B ) i^i ( _V \ C ) ) ) = ( A \ ( _V \ ( ( _V \ B ) i^i ( _V \ C ) ) ) )
5 invdif 
 |-  ( A i^i ( _V \ B ) ) = ( A \ B )
6 invdif 
 |-  ( A i^i ( _V \ C ) ) = ( A \ C )
7 5 6 ineq12i 
 |-  ( ( A i^i ( _V \ B ) ) i^i ( A i^i ( _V \ C ) ) ) = ( ( A \ B ) i^i ( A \ C ) )
8 3 4 7 3eqtr3i 
 |-  ( A \ ( _V \ ( ( _V \ B ) i^i ( _V \ C ) ) ) ) = ( ( A \ B ) i^i ( A \ C ) )
9 2 8 eqtri 
 |-  ( A \ ( B u. C ) ) = ( ( A \ B ) i^i ( A \ C ) )