Metamath Proof Explorer

Theorem difindi

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

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

Proof

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