Theorem dfarea

Description: Rewrite df-area self-referentially. (Contributed by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Assertion	dfarea	|- area = ( s e. dom area |-> S. RR ( vol ` ( s " { x } ) ) _d x )

Proof

Step	Hyp	Ref	Expression
1		df-area	|- area = ( s e. { y e. ~P ( RR X. RR ) | ( A. x e. RR ( y " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( y " { x } ) ) ) e. L^1 ) } |-> S. RR ( vol ` ( s " { x } ) ) _d x )
2		itgex	|- S. RR ( vol ` ( s " { x } ) ) _d x e. _V
3	2 1	dmmpti	|- dom area = { y e. ~P ( RR X. RR ) | ( A. x e. RR ( y " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( y " { x } ) ) ) e. L^1 ) }
4	3	mpteq1i	|- ( s e. dom area |-> S. RR ( vol ` ( s " { x } ) ) _d x ) = ( s e. { y e. ~P ( RR X. RR ) | ( A. x e. RR ( y " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( y " { x } ) ) ) e. L^1 ) } |-> S. RR ( vol ` ( s " { x } ) ) _d x )
5	1 4	eqtr4i	|- area = ( s e. dom area |-> S. RR ( vol ` ( s " { x } ) ) _d x )