This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem indifcom

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

		Ref	Expression
	Assertion	indifcom	$⊢ A \cap (B ∖ C) = B \cap (A ∖ C)$

Step	Hyp	Ref	Expression
1		incom	$⊢ A \cap B = B \cap A$
2	1	difeq1i	$⊢ (A \cap B) ∖ C = (B \cap A) ∖ C$
3		indif2	$⊢ A \cap (B ∖ C) = (A \cap B) ∖ C$
4		indif2	$⊢ B \cap (A ∖ C) = (B \cap A) ∖ C$
5	2 3 4	3eqtr4i	$⊢ A \cap (B ∖ C) = B \cap (A ∖ C)$