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

Definition df-cbn 22365
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 22364 . 2  class  CBan
2 vu . . . . . 6  set  u
32cv 1651 . . . . 5  class  u
4 cims 22070 . . . . 5  class  IndMet
53, 4cfv 5454 . . . 4  class  ( IndMet `  u )
6 cba 22065 . . . . . 6  class  BaseSet
73, 6cfv 5454 . . . . 5  class  ( BaseSet `  u )
8 cms 19207 . . . . 5  class  CMet
97, 8cfv 5454 . . . 4  class  ( CMet `  ( BaseSet `  u )
)
105, 9wcel 1725 . . 3  wff  ( IndMet `  u )  e.  (
CMet `  ( BaseSet `  u
) )
11 cnv 22063 . . 3  class  NrmCVec
1210, 2, 11crab 2709 . 2  class  { u  e.  NrmCVec  |  ( IndMet `  u )  e.  (
CMet `  ( BaseSet `  u
) ) }
131, 12wceq 1652 1  wff  CBan  =  { u  e.  NrmCVec  |  (
IndMet `  u )  e.  ( CMet `  ( BaseSet
`  u ) ) }
Colors of variables: wff set class
This definition is referenced by:  iscbn  22366
  Copyright terms: Public domain W3C validator