Metamath Proof Explorer

Theorem difmbl

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

Ref Expression
Assertion difmbl ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol → A ∖ B ∈ dom ⁡ vol

Proof

Step Hyp Ref Expression
1 indif2 ⊢ A ∩ ℝ ∖ B = A ∩ ℝ ∖ B
2 mblss ⊢ A ∈ dom ⁡ vol → A ⊆ ℝ
3 dfss2 ⊢ A ⊆ ℝ ↔ A ∩ ℝ = A
4 2 3 sylib ⊢ A ∈ dom ⁡ vol → A ∩ ℝ = A
5 4 difeq1d ⊢ A ∈ dom ⁡ vol → A ∩ ℝ ∖ B = A ∖ B
6 1 5 eqtrid ⊢ A ∈ dom ⁡ vol → A ∩ ℝ ∖ B = A ∖ B
7 6 adantr ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol → A ∩ ℝ ∖ B = A ∖ B
8 cmmbl ⊢ B ∈ dom ⁡ vol → ℝ ∖ B ∈ dom ⁡ vol
9 inmbl ⊢ A ∈ dom ⁡ vol ∧ ℝ ∖ B ∈ dom ⁡ vol → A ∩ ℝ ∖ B ∈ dom ⁡ vol
10 8 9 sylan2 ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol → A ∩ ℝ ∖ B ∈ dom ⁡ vol
11 7 10 eqeltrrd ⊢ A ∈ dom ⁡ vol ∧ B ∈ dom ⁡ vol → A ∖ B ∈ dom ⁡ vol