Metamath Proof Explorer


Theorem difundir

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

Ref Expression
Assertion difundir ( ( 𝐴𝐵 ) ∖ 𝐶 ) = ( ( 𝐴𝐶 ) ∪ ( 𝐵𝐶 ) )

Proof

Step Hyp Ref Expression
1 indir ( ( 𝐴𝐵 ) ∩ ( V ∖ 𝐶 ) ) = ( ( 𝐴 ∩ ( V ∖ 𝐶 ) ) ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) )
2 invdif ( ( 𝐴𝐵 ) ∩ ( V ∖ 𝐶 ) ) = ( ( 𝐴𝐵 ) ∖ 𝐶 )
3 invdif ( 𝐴 ∩ ( V ∖ 𝐶 ) ) = ( 𝐴𝐶 )
4 invdif ( 𝐵 ∩ ( V ∖ 𝐶 ) ) = ( 𝐵𝐶 )
5 3 4 uneq12i ( ( 𝐴 ∩ ( V ∖ 𝐶 ) ) ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) = ( ( 𝐴𝐶 ) ∪ ( 𝐵𝐶 ) )
6 1 2 5 3eqtr3i ( ( 𝐴𝐵 ) ∖ 𝐶 ) = ( ( 𝐴𝐶 ) ∪ ( 𝐵𝐶 ) )