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 
|- BrSiga C_ ~P RR

Proof

Step Hyp Ref Expression
1 brsigarn 
 |-  BrSiga e. ( sigAlgebra ` RR )
2 sigasspw 
 |-  ( BrSiga e. ( sigAlgebra ` RR ) -> BrSiga C_ ~P RR )
3 1 2 ax-mp 
 |-  BrSiga C_ ~P RR