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

Definition df-cau 21166
Description: Define a function on metric spaces whose value is the set of Cauchy sequences of the space. (Contributed by NM, 8-Sep-2006.)
Assertion
Ref Expression
df-cau
Distinct variable group:   , , ,

Detailed syntax breakdown of Definition df-cau
StepHypRef Expression
1 cca 21163 . 2
2 vd . . 3
3 cxmt 17994 . . . . 5
43crn 4958 . . . 4
54cuni 4208 . . 3
6 vj . . . . . . . . 9
76cv 1369 . . . . . . . 8
8 cuz 11000 . . . . . . . 8
97, 8cfv 5537 . . . . . . 7
10 vf . . . . . . . . . 10
1110cv 1369 . . . . . . . . 9
127, 11cfv 5537 . . . . . . . 8
13 vx . . . . . . . . 9
1413cv 1369 . . . . . . . 8
152cv 1369 . . . . . . . . 9
16 cbl 17996 . . . . . . . . 9
1715, 16cfv 5537 . . . . . . . 8
1812, 14, 17co 6222 . . . . . . 7
1911, 9cres 4959 . . . . . . 7
209, 18, 19wf 5533 . . . . . 6
21 cz 10784 . . . . . 6
2220, 6, 21wrex 2801 . . . . 5
23 crp 11130 . . . . 5
2422, 13, 23wral 2800 . . . 4
2515cdm 4957 . . . . . 6
2625cdm 4957 . . . . 5
27 cc 9417 . . . . 5
28 cpm 7349 . . . . 5
2926, 27, 28co 6222 . . . 4
3024, 10, 29crab 2804 . . 3
312, 5, 30cmpt 4467 . 2
321, 31wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  caufval  21185
  Copyright terms: Public domain W3C validator