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		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))$
6		elin	$⊢ x \in ((C ∖ B) \cap A) \leftrightarrow (x \in (C ∖ B) \land x \in A)$
7		eldif	$⊢ x \in (C ∖ B) \leftrightarrow (x \in C \land \neg x \in B)$
8	6 7	bianbi	$⊢ x \in ((C ∖ B) \cap A) \leftrightarrow ((x \in C \land \neg x \in B) \land x \in A)$
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	5 8 9	3bitr4i	$⊢ x \in ((C ∖ B) \cap A) \leftrightarrow ((x \in A \land x \in C) \land \neg x \in B)$
11	3 4 10	3bitr4g	$⊢ A \subseteq C \to (x \in (A ∖ B) \leftrightarrow x \in ((C ∖ B) \cap A))$
12	11	eqrdv	$⊢ A \subseteq C \to A ∖ B = (C ∖ B) \cap A$

Metamath Proof Explorer