Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-area Structured version   Unicode version

Definition df-area 20787
 Description: Define the area of a subset of . (Contributed by Mario Carneiro, 21-Jun-2015.)
Assertion
Ref Expression
df-area area
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-area
StepHypRef Expression
1 carea 20786 . 2 area
2 vs . . 3
3 vt . . . . . . . . 9
43cv 1651 . . . . . . . 8
5 vx . . . . . . . . . 10
65cv 1651 . . . . . . . . 9
76csn 3806 . . . . . . . 8
84, 7cima 4873 . . . . . . 7
9 cvol 19352 . . . . . . . . 9
109ccnv 4869 . . . . . . . 8
11 cr 8981 . . . . . . . 8
1210, 11cima 4873 . . . . . . 7
138, 12wcel 1725 . . . . . 6
1413, 5, 11wral 2697 . . . . 5
158, 9cfv 5446 . . . . . . 7
165, 11, 15cmpt 4258 . . . . . 6
17 cibl 19501 . . . . . 6
1816, 17wcel 1725 . . . . 5
1914, 18wa 359 . . . 4
2011, 11cxp 4868 . . . . 5
2120cpw 3791 . . . 4
2219, 3, 21crab 2701 . . 3
232cv 1651 . . . . . 6
2423, 7cima 4873 . . . . 5
2524, 9cfv 5446 . . . 4
265, 11, 25citg 19502 . . 3
272, 22, 26cmpt 4258 . 2
281, 27wceq 1652 1 area
 Colors of variables: wff set class This definition is referenced by:  dmarea  20788  dfarea  20791
 Copyright terms: Public domain W3C validator