Metamath Proof Explorer


Theorem difindir

Description: Distributive law for class difference. (Contributed by NM, 17-Aug-2004)

Ref Expression
Assertion difindir
|- ( ( A i^i B ) \ C ) = ( ( A \ C ) i^i ( B \ C ) )

Proof

Step Hyp Ref Expression
1 inindir
 |-  ( ( A i^i B ) i^i ( _V \ C ) ) = ( ( A i^i ( _V \ C ) ) i^i ( B i^i ( _V \ C ) ) )
2 invdif
 |-  ( ( A i^i B ) i^i ( _V \ C ) ) = ( ( A i^i B ) \ C )
3 invdif
 |-  ( A i^i ( _V \ C ) ) = ( A \ C )
4 invdif
 |-  ( B i^i ( _V \ C ) ) = ( B \ C )
5 3 4 ineq12i
 |-  ( ( A i^i ( _V \ C ) ) i^i ( B i^i ( _V \ C ) ) ) = ( ( A \ C ) i^i ( B \ C ) )
6 1 2 5 3eqtr3i
 |-  ( ( A i^i B ) \ C ) = ( ( A \ C ) i^i ( B \ C ) )