Theorem difmbl

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

	Ref	Expression
Assertion	difmbl	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( 𝐴 ∖ 𝐵 ) ∈ dom vol )

Proof

Step	Hyp	Ref	Expression
1		indif2	⊢ ( 𝐴 ∩ ( ℝ ∖ 𝐵 ) ) = ( ( 𝐴 ∩ ℝ ) ∖ 𝐵 )
2		mblss	⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
3		df-ss	⊢ ( 𝐴 ⊆ ℝ ↔ ( 𝐴 ∩ ℝ ) = 𝐴 )
4	2 3	sylib	⊢ ( 𝐴 ∈ dom vol → ( 𝐴 ∩ ℝ ) = 𝐴 )
5	4	difeq1d	⊢ ( 𝐴 ∈ dom vol → ( ( 𝐴 ∩ ℝ ) ∖ 𝐵 ) = ( 𝐴 ∖ 𝐵 ) )
6	1 5	eqtrid	⊢ ( 𝐴 ∈ dom vol → ( 𝐴 ∩ ( ℝ ∖ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 ) )
7	6	adantr	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( 𝐴 ∩ ( ℝ ∖ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 ) )
8		cmmbl	⊢ ( 𝐵 ∈ dom vol → ( ℝ ∖ 𝐵 ) ∈ dom vol )
9		inmbl	⊢ ( ( 𝐴 ∈ dom vol ∧ ( ℝ ∖ 𝐵 ) ∈ dom vol ) → ( 𝐴 ∩ ( ℝ ∖ 𝐵 ) ) ∈ dom vol )
10	8 9	sylan2	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( 𝐴 ∩ ( ℝ ∖ 𝐵 ) ) ∈ dom vol )
11	7 10	eqeltrrd	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( 𝐴 ∖ 𝐵 ) ∈ dom vol )