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

Metamath Proof Explorer

Theorem difin

Description: Difference with intersection. Theorem 33 of Suppes p. 29. (Contributed by NM, 31-Mar-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		pm4.61	$⊢ \neg (x \in A \to x \in B) \leftrightarrow (x \in A \land \neg x \in B)$
2		anclb	$⊢ (x \in A \to x \in B) \leftrightarrow (x \in A \to (x \in A \land x \in B))$
3		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
4	3	imbi2i	$⊢ (x \in A \to x \in (A \cap B)) \leftrightarrow (x \in A \to (x \in A \land x \in B))$
5		iman	$⊢ (x \in A \to x \in (A \cap B)) \leftrightarrow \neg (x \in A \land \neg x \in (A \cap B))$
6	2 4 5	3bitr2i	$⊢ (x \in A \to x \in B) \leftrightarrow \neg (x \in A \land \neg x \in (A \cap B))$
7	6	con2bii	$⊢ (x \in A \land \neg x \in (A \cap B)) \leftrightarrow \neg (x \in A \to x \in B)$
8		eldif	$⊢ x \in (A ∖ B) \leftrightarrow (x \in A \land \neg x \in B)$
9	1 7 8	3bitr4i	$⊢ (x \in A \land \neg x \in (A \cap B)) \leftrightarrow x \in (A ∖ B)$
10	9	difeqri	$⊢ A ∖ (A \cap B) = A ∖ B$