Metamath Proof Explorer

Theorem brsigasspwrn

Description: The Borel Algebra is a set of subsets of the real numbers. (Contributed by Thierry Arnoux, 19-Jan-2017)

		Ref	Expression
	Assertion	brsigasspwrn	$⊢ 𝔅_{ℝ} \subseteq 𝒫 ℝ$

Step	Hyp	Ref	Expression
1		brsigarn	$⊢ 𝔅_{ℝ} \in sigAlgebra (ℝ)$
2		sigasspw	$⊢ 𝔅_{ℝ} \in sigAlgebra (ℝ) \to 𝔅_{ℝ} \subseteq 𝒫 ℝ$
3	1 2	ax-mp	$⊢ 𝔅_{ℝ} \subseteq 𝒫 ℝ$