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

Definition df-ds 14200
Description: Define the distance function component of a metric space (structure). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
df-ds

Detailed syntax breakdown of Definition df-ds
StepHypRef Expression
1 cds 14187 . 2
2 c1 9229 . . . 4
3 c2 10317 . . . 4
42, 3cdc 10700 . . 3
54cslot 14113 . 2
61, 5wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  dsndx  14281  dsid  14282  ressds  14292  mgpds  16467  srads  17076  tmslem  19757  tngds  19934  ttgds  22806
  Copyright terms: Public domain W3C validator