Metamath Proof Explorer

Theorem difun1

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

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

Proof

Step Hyp Ref Expression
1 inass ⊢ ( ( 𝐴 ∩ ( V ∖ 𝐵 ) ) ∩ ( V ∖ 𝐶 ) ) = ( 𝐴 ∩ ( ( V ∖ 𝐵 ) ∩ ( V ∖ 𝐶 ) ) )
2 invdif ⊢ ( ( 𝐴 ∩ ( V ∖ 𝐵 ) ) ∩ ( V ∖ 𝐶 ) ) = ( ( 𝐴 ∩ ( V ∖ 𝐵 ) ) ∖ 𝐶 )
3 1 2 eqtr3i ⊢ ( 𝐴 ∩ ( ( V ∖ 𝐵 ) ∩ ( V ∖ 𝐶 ) ) ) = ( ( 𝐴 ∩ ( V ∖ 𝐵 ) ) ∖ 𝐶 )
4 undm ⊢ ( V ∖ ( 𝐵 ∪ 𝐶 ) ) = ( ( V ∖ 𝐵 ) ∩ ( V ∖ 𝐶 ) )
5 4 ineq2i ⊢ ( 𝐴 ∩ ( V ∖ ( 𝐵 ∪ 𝐶 ) ) ) = ( 𝐴 ∩ ( ( V ∖ 𝐵 ) ∩ ( V ∖ 𝐶 ) ) )
6 invdif ⊢ ( 𝐴 ∩ ( V ∖ ( 𝐵 ∪ 𝐶 ) ) ) = ( 𝐴 ∖ ( 𝐵 ∪ 𝐶 ) )
7 5 6 eqtr3i ⊢ ( 𝐴 ∩ ( ( V ∖ 𝐵 ) ∩ ( V ∖ 𝐶 ) ) ) = ( 𝐴 ∖ ( 𝐵 ∪ 𝐶 ) )
8 3 7 eqtr3i ⊢ ( ( 𝐴 ∩ ( V ∖ 𝐵 ) ) ∖ 𝐶 ) = ( 𝐴 ∖ ( 𝐵 ∪ 𝐶 ) )
9 invdif ⊢ ( 𝐴 ∩ ( V ∖ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 )
10 9 difeq1i ⊢ ( ( 𝐴 ∩ ( V ∖ 𝐵 ) ) ∖ 𝐶 ) = ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 )
11 8 10 eqtr3i ⊢ ( 𝐴 ∖ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 )