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

Definition df-cbn 30116
Description: Define the class of all complex Banach spaces. (Contributed by NM, 5-Dec-2006.) Use df-bn 24853 instead. (New usage is discouraged.)
Assertion
Ref Expression
df-cbn CBan = {𝑢 ∈ NrmCVec ∣ (IndMet‘𝑢) ∈ (CMet‘(BaseSet‘𝑢))}

Detailed syntax breakdown of Definition df-cbn
StepHypRef Expression
1 ccbn 30115 . 2 class CBan
2 vu . . . . . 6 setvar 𝑢
32cv 1541 . . . . 5 class 𝑢
4 cims 29844 . . . . 5 class IndMet
53, 4cfv 6544 . . . 4 class (IndMet‘𝑢)
6 cba 29839 . . . . . 6 class BaseSet
73, 6cfv 6544 . . . . 5 class (BaseSet‘𝑢)
8 ccmet 24771 . . . . 5 class CMet
97, 8cfv 6544 . . . 4 class (CMet‘(BaseSet‘𝑢))
105, 9wcel 2107 . . 3 wff (IndMet‘𝑢) ∈ (CMet‘(BaseSet‘𝑢))
11 cnv 29837 . . 3 class NrmCVec
1210, 2, 11crab 3433 . 2 class {𝑢 ∈ NrmCVec ∣ (IndMet‘𝑢) ∈ (CMet‘(BaseSet‘𝑢))}
131, 12wceq 1542 1 wff CBan = {𝑢 ∈ NrmCVec ∣ (IndMet‘𝑢) ∈ (CMet‘(BaseSet‘𝑢))}
Colors of variables: wff setvar class
This definition is referenced by:  iscbn  30117
  Copyright terms: Public domain W3C validator