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

Metamath Proof Explorer

Theorem difun1

Description: A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004)

Ref Expression
Assertion difun1 
|- ( A \ ( B u. C ) ) = ( ( A \ B ) \ C )

Proof

Step Hyp Ref Expression
1 inass 
 |-  ( ( A i^i ( _V \ B ) ) i^i ( _V \ C ) ) = ( A i^i ( ( _V \ B ) i^i ( _V \ C ) ) )
2 invdif 
 |-  ( ( A i^i ( _V \ B ) ) i^i ( _V \ C ) ) = ( ( A i^i ( _V \ B ) ) \ C )
3 1 2 eqtr3i 
 |-  ( A i^i ( ( _V \ B ) i^i ( _V \ C ) ) ) = ( ( A i^i ( _V \ B ) ) \ C )
4 undm 
 |-  ( _V \ ( B u. C ) ) = ( ( _V \ B ) i^i ( _V \ C ) )
5 4 ineq2i 
 |-  ( A i^i ( _V \ ( B u. C ) ) ) = ( A i^i ( ( _V \ B ) i^i ( _V \ C ) ) )
6 invdif 
 |-  ( A i^i ( _V \ ( B u. C ) ) ) = ( A \ ( B u. C ) )
7 5 6 eqtr3i 
 |-  ( A i^i ( ( _V \ B ) i^i ( _V \ C ) ) ) = ( A \ ( B u. C ) )
8 3 7 eqtr3i 
 |-  ( ( A i^i ( _V \ B ) ) \ C ) = ( A \ ( B u. C ) )
9 invdif 
 |-  ( A i^i ( _V \ B ) ) = ( A \ B )
10 9 difeq1i 
 |-  ( ( A i^i ( _V \ B ) ) \ C ) = ( ( A \ B ) \ C )
11 8 10 eqtr3i 
 |-  ( A \ ( B u. C ) ) = ( ( A \ B ) \ C )