Metamath Proof Explorer

Theorem difmbl

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

Ref Expression
Assertion difmbl ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\right)\to {A}\setminus {B}\in \mathrm{dom}vol$

Proof

Step Hyp Ref Expression
1 indif2 ${⊢}{A}\cap \left(ℝ\setminus {B}\right)=\left({A}\cap ℝ\right)\setminus {B}$
2 mblss ${⊢}{A}\in \mathrm{dom}vol\to {A}\subseteq ℝ$
3 df-ss ${⊢}{A}\subseteq ℝ↔{A}\cap ℝ={A}$
4 2 3 sylib ${⊢}{A}\in \mathrm{dom}vol\to {A}\cap ℝ={A}$
5 4 difeq1d ${⊢}{A}\in \mathrm{dom}vol\to \left({A}\cap ℝ\right)\setminus {B}={A}\setminus {B}$
6 1 5 syl5eq ${⊢}{A}\in \mathrm{dom}vol\to {A}\cap \left(ℝ\setminus {B}\right)={A}\setminus {B}$
7 6 adantr ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\right)\to {A}\cap \left(ℝ\setminus {B}\right)={A}\setminus {B}$
8 cmmbl ${⊢}{B}\in \mathrm{dom}vol\to ℝ\setminus {B}\in \mathrm{dom}vol$
9 inmbl ${⊢}\left({A}\in \mathrm{dom}vol\wedge ℝ\setminus {B}\in \mathrm{dom}vol\right)\to {A}\cap \left(ℝ\setminus {B}\right)\in \mathrm{dom}vol$
10 8 9 sylan2 ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\right)\to {A}\cap \left(ℝ\setminus {B}\right)\in \mathrm{dom}vol$
11 7 10 eqeltrrd ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\in \mathrm{dom}vol\right)\to {A}\setminus {B}\in \mathrm{dom}vol$