difin2

Description: Represent a class difference as an intersection with a larger difference. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	difin2	$⊢ A \subseteq C \to A ∖ B = (C ∖ B) \cap A$

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq C \to (x \in A \to x \in C)$
2	1	pm4.71d	$⊢ A \subseteq C \to (x \in A \leftrightarrow (x \in A \land x \in C))$
3	2	anbi1d	$⊢ A \subseteq C \to ((x \in A \land \neg x \in B) \leftrightarrow ((x \in A \land x \in C) \land \neg x \in B))$
4		eldif	$⊢ x \in (A ∖ B) \leftrightarrow (x \in A \land \neg x \in B)$
5		elin	$⊢ x \in ((C ∖ B) \cap A) \leftrightarrow (x \in (C ∖ B) \land x \in A)$
6		eldif	$⊢ x \in (C ∖ B) \leftrightarrow (x \in C \land \neg x \in B)$
7	6	anbi1i	$⊢ (x \in (C ∖ B) \land x \in A) \leftrightarrow ((x \in C \land \neg x \in B) \land x \in A)$
8		ancom	$⊢ ((x \in C \land \neg x \in B) \land x \in A) \leftrightarrow (x \in A \land (x \in C \land \neg x \in B))$
9		anass	$⊢ ((x \in A \land x \in C) \land \neg x \in B) \leftrightarrow (x \in A \land (x \in C \land \neg x \in B))$
10	8 9	bitr4i	$⊢ ((x \in C \land \neg x \in B) \land x \in A) \leftrightarrow ((x \in A \land x \in C) \land \neg x \in B)$
11	5 7 10	3bitri	$⊢ x \in ((C ∖ B) \cap A) \leftrightarrow ((x \in A \land x \in C) \land \neg x \in B)$
12	3 4 11	3bitr4g	$⊢ A \subseteq C \to (x \in (A ∖ B) \leftrightarrow x \in ((C ∖ B) \cap A))$
13	12	eqrdv	$⊢ A \subseteq C \to A ∖ B = (C ∖ B) \cap A$

Metamath Proof Explorer