Metamath Proof Explorer


Definition df-area

Description: Define the area of a subset of RR X. RR . (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion df-area area = s t 𝒫 2 | x t x vol -1 x vol t x 𝐿 1 vol s x dx

Detailed syntax breakdown

Step Hyp Ref Expression
0 carea class area
1 vs setvar s
2 vt setvar t
3 cr class
4 3 3 cxp class 2
5 4 cpw class 𝒫 2
6 vx setvar x
7 2 cv setvar t
8 6 cv setvar x
9 8 csn class x
10 7 9 cima class t x
11 cvol class vol
12 11 ccnv class vol -1
13 12 3 cima class vol -1
14 10 13 wcel wff t x vol -1
15 14 6 3 wral wff x t x vol -1
16 10 11 cfv class vol t x
17 6 3 16 cmpt class x vol t x
18 cibl class 𝐿 1
19 17 18 wcel wff x vol t x 𝐿 1
20 15 19 wa wff x t x vol -1 x vol t x 𝐿 1
21 20 2 5 crab class t 𝒫 2 | x t x vol -1 x vol t x 𝐿 1
22 1 cv setvar s
23 22 9 cima class s x
24 23 11 cfv class vol s x
25 6 3 24 citg class vol s x dx
26 1 21 25 cmpt class s t 𝒫 2 | x t x vol -1 x vol t x 𝐿 1 vol s x dx
27 0 26 wceq wff area = s t 𝒫 2 | x t x vol -1 x vol t x 𝐿 1 vol s x dx