Theorem dif32

Description: Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004)

	Ref	Expression
Assertion	dif32	⊢ ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) = ( ( 𝐴 ∖ 𝐶 ) ∖ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		uncom	⊢ ( 𝐵 ∪ 𝐶 ) = ( 𝐶 ∪ 𝐵 )
2	1	difeq2i	⊢ ( 𝐴 ∖ ( 𝐵 ∪ 𝐶 ) ) = ( 𝐴 ∖ ( 𝐶 ∪ 𝐵 ) )
3		difun1	⊢ ( 𝐴 ∖ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 )
4		difun1	⊢ ( 𝐴 ∖ ( 𝐶 ∪ 𝐵 ) ) = ( ( 𝐴 ∖ 𝐶 ) ∖ 𝐵 )
5	2 3 4	3eqtr3i	⊢ ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐶 ) = ( ( 𝐴 ∖ 𝐶 ) ∖ 𝐵 )