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

Definition df-cbn 23386
Description: Define the class of all complex Banach spaces. (Contributed by NM, 5-Dec-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-cbn

Detailed syntax breakdown of Definition df-cbn
StepHypRef Expression
1 ccbn 23385 . 2
2 vu . . . . . 6
32cv 1669 . . . . 5
4 cims 23091 . . . . 5
53, 4cfv 5438 . . . 4
6 cba 23086 . . . . . 6
73, 6cfv 5438 . . . . 5
8 cms 20222 . . . . 5
97, 8cfv 5438 . . . 4
105, 9wcel 1732 . . 3
11 cnv 23084 . . 3
1210, 2, 11crab 2763 . 2
131, 12wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  iscbn  23387
  Copyright terms: Public domain W3C validator