Theorem dmvolss

Description: Lebesgue measurable sets are subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Assertion	dmvolss	|- dom vol C_ ~P RR

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( x e. dom vol -> x e. _V )
2		mblss	|- ( x e. dom vol -> x C_ RR )
3	1 2	elpwd	|- ( x e. dom vol -> x e. ~P RR )
4	3	rgen	|- A. x e. dom vol x e. ~P RR
5		dfss3	|- ( dom vol C_ ~P RR <-> A. x e. dom vol x e. ~P RR )
6	4 5	mpbir	|- dom vol C_ ~P RR