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

Definition df-cbn 21436
Description: Define the class of all complex Banach spaces. (Contributed by NM, 5-Dec-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-cbn  |-  CBan  =  { u  e.  NrmCVec  |  (
IndMet `  u )  e.  ( CMet `  ( BaseSet
`  u ) ) }

Detailed syntax breakdown of Definition df-cbn
StepHypRef Expression
1 ccbn 21435 . 2  class  CBan
2 vu . . . . . 6  set  u
32cv 1622 . . . . 5  class  u
4 cims 21141 . . . . 5  class  IndMet
53, 4cfv 5221 . . . 4  class  ( IndMet `  u )
6 cba 21136 . . . . . 6  class  BaseSet
73, 6cfv 5221 . . . . 5  class  ( BaseSet `  u )
8 cms 18676 . . . . 5  class  CMet
97, 8cfv 5221 . . . 4  class  ( CMet `  ( BaseSet `  u )
)
105, 9wcel 1685 . . 3  wff  ( IndMet `  u )  e.  (
CMet `  ( BaseSet `  u
) )
11 cnv 21134 . . 3  class  NrmCVec
1210, 2, 11crab 2548 . 2  class  { u  e.  NrmCVec  |  ( IndMet `  u )  e.  (
CMet `  ( BaseSet `  u
) ) }
131, 12wceq 1623 1  wff  CBan  =  { u  e.  NrmCVec  |  (
IndMet `  u )  e.  ( CMet `  ( BaseSet
`  u ) ) }
Colors of variables: wff set class
This definition is referenced by:  iscbn  21437
  Copyright terms: Public domain W3C validator