difmbl

Description: A difference of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014)

		Ref	Expression
	Assertion	difmbl	$⊢ (A \in dom vol \land B \in dom vol) \to A ∖ B \in dom vol$

Step	Hyp	Ref	Expression
1		indif2	$⊢ A \cap (ℝ ∖ B) = (A \cap ℝ) ∖ B$
2		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
3		df-ss	$⊢ A \subseteq ℝ \leftrightarrow A \cap ℝ = A$
4	2 3	sylib	$⊢ A \in dom vol \to A \cap ℝ = A$
5	4	difeq1d	$⊢ A \in dom vol \to (A \cap ℝ) ∖ B = A ∖ B$
6	1 5	eqtrid	$⊢ A \in dom vol \to A \cap (ℝ ∖ B) = A ∖ B$
7	6	adantr	$⊢ (A \in dom vol \land B \in dom vol) \to A \cap (ℝ ∖ B) = A ∖ B$
8		cmmbl	$⊢ B \in dom vol \to ℝ ∖ B \in dom vol$
9		inmbl	$⊢ (A \in dom vol \land ℝ ∖ B \in dom vol) \to A \cap (ℝ ∖ B) \in dom vol$
10	8 9	sylan2	$⊢ (A \in dom vol \land B \in dom vol) \to A \cap (ℝ ∖ B) \in dom vol$
11	7 10	eqeltrrd	$⊢ (A \in dom vol \land B \in dom vol) \to A ∖ B \in dom vol$

Metamath Proof Explorer