Metamath Proof Explorer

Theorem areass

Description: A measurable region is a subset of RR X. RR . (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion areass 
|- ( S e. dom area -> S C_ ( RR X. RR ) )

Proof

Step Hyp Ref Expression
1 dmarea 
 |-  ( S e. dom area <-> ( S C_ ( RR X. RR ) /\ A. x e. RR ( S " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1 ) )
2 1 simp1bi 
 |-  ( S e. dom area -> S C_ ( RR X. RR ) )