Theorem snmbl

Description: A singleton is measurable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	snmbl	⊢ ( 𝐴 ∈ ℝ → { 𝐴 } ∈ dom vol )

Proof

Step	Hyp	Ref	Expression
1		snssi	⊢ ( 𝐴 ∈ ℝ → { 𝐴 } ⊆ ℝ )
2		ovolsn	⊢ ( 𝐴 ∈ ℝ → ( vol* ‘ { 𝐴 } ) = 0 )
3		nulmbl	⊢ ( ( { 𝐴 } ⊆ ℝ ∧ ( vol* ‘ { 𝐴 } ) = 0 ) → { 𝐴 } ∈ dom vol )
4	1 2 3	syl2anc	⊢ ( 𝐴 ∈ ℝ → { 𝐴 } ∈ dom vol )