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

Definition df-cau 19260
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 19257 . 2
2 vd . . 3
3 cxmt 16737 . . . . 5
43crn 4920 . . . 4
54cuni 4043 . . 3
6 vj . . . . . . . . 9
76cv 1653 . . . . . . . 8
8 cuz 10539 . . . . . . . 8
97, 8cfv 5501 . . . . . . 7
10 vf . . . . . . . . . 10
1110cv 1653 . . . . . . . . 9
127, 11cfv 5501 . . . . . . . 8
13 vx . . . . . . . . 9
1413cv 1653 . . . . . . . 8
152cv 1653 . . . . . . . . 9
16 cbl 16739 . . . . . . . . 9
1715, 16cfv 5501 . . . . . . . 8
1812, 14, 17co 6129 . . . . . . 7
1911, 9cres 4921 . . . . . . 7
209, 18, 19wf 5497 . . . . . 6
21 cz 10333 . . . . . 6
2220, 6, 21wrex 2713 . . . . 5
23 crp 10663 . . . . 5
2422, 13, 23wral 2712 . . . 4
2515cdm 4919 . . . . . 6
2625cdm 4919 . . . . 5
27 cc 9039 . . . . 5
28 cpm 7068 . . . . 5
2926, 27, 28co 6129 . . . 4
3024, 10, 29crab 2716 . . 3
312, 5, 30cmpt 4301 . 2
321, 31wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  caufval  19279
  Copyright terms: Public domain W3C validator