Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bnd Structured version   Unicode version

Definition df-bnd 31844
 Description: Define the class of bounded metrics. A metric space is bounded iff it can be covered by a single ball. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
df-bnd
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-bnd
StepHypRef Expression
1 cbnd 31832 . 2
2 vx . . 3
3 cvv 3078 . . 3
42cv 1436 . . . . . . 7
5 vy . . . . . . . . 9
65cv 1436 . . . . . . . 8
7 vr . . . . . . . . 9
87cv 1436 . . . . . . . 8
9 vm . . . . . . . . . 10
109cv 1436 . . . . . . . . 9
11 cbl 18885 . . . . . . . . 9
1210, 11cfv 5592 . . . . . . . 8
136, 8, 12co 6296 . . . . . . 7
144, 13wceq 1437 . . . . . 6
15 crp 11291 . . . . . 6
1614, 7, 15wrex 2774 . . . . 5
1716, 5, 4wral 2773 . . . 4
18 cme 18884 . . . . 5
194, 18cfv 5592 . . . 4
2017, 9, 19crab 2777 . . 3
212, 3, 20cmpt 4475 . 2
221, 21wceq 1437 1
 Colors of variables: wff setvar class This definition is referenced by:  isbnd  31845
 Copyright terms: Public domain W3C validator