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

Metamath Proof Explorer

Theorem indif

Description: Intersection with class difference. Theorem 34 of Suppes p. 29. (Contributed by NM, 17-Aug-2004)

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

Step	Hyp	Ref	Expression
1		dfin4	$⊢ A \cap (A ∖ B) = A ∖ (A ∖ (A ∖ B))$
2		dfin4	$⊢ A \cap B = A ∖ (A ∖ B)$
3	2	difeq2i	$⊢ A ∖ (A \cap B) = A ∖ (A ∖ (A ∖ B))$
4		difin	$⊢ A ∖ (A \cap B) = A ∖ B$
5	1 3 4	3eqtr2i	$⊢ A \cap (A ∖ B) = A ∖ B$