Theorem indifcom

Description: Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013)

	Ref	Expression
Assertion	indifcom	⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) = ( 𝐵 ∩ ( 𝐴 ∖ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		incom	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
2	1	difeq1i	⊢ ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) = ( ( 𝐵 ∩ 𝐴 ) ∖ 𝐶 )
3		indif2	⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 )
4		indif2	⊢ ( 𝐵 ∩ ( 𝐴 ∖ 𝐶 ) ) = ( ( 𝐵 ∩ 𝐴 ) ∖ 𝐶 )
5	2 3 4	3eqtr4i	⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐶 ) ) = ( 𝐵 ∩ ( 𝐴 ∖ 𝐶 ) )