# Metamath Proof Explorer

## Definition df-cbn

Description: Define the class of all complex Banach spaces. (Contributed by NM, 5-Dec-2006) Use df-bn instead. (New usage is discouraged.)

Ref Expression
Assertion df-cbn ${⊢}\mathrm{CBan}=\left\{{u}\in \mathrm{NrmCVec}|\mathrm{IndMet}\left({u}\right)\in \mathrm{CMet}\left(\mathrm{BaseSet}\left({u}\right)\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ccbn ${class}\mathrm{CBan}$
1 vu ${setvar}{u}$
2 cnv ${class}\mathrm{NrmCVec}$
3 cims ${class}\mathrm{IndMet}$
4 1 cv ${setvar}{u}$
5 4 3 cfv ${class}\mathrm{IndMet}\left({u}\right)$
6 ccmet ${class}\mathrm{CMet}$
7 cba ${class}\mathrm{BaseSet}$
8 4 7 cfv ${class}\mathrm{BaseSet}\left({u}\right)$
9 8 6 cfv ${class}\mathrm{CMet}\left(\mathrm{BaseSet}\left({u}\right)\right)$
10 5 9 wcel ${wff}\mathrm{IndMet}\left({u}\right)\in \mathrm{CMet}\left(\mathrm{BaseSet}\left({u}\right)\right)$
11 10 1 2 crab ${class}\left\{{u}\in \mathrm{NrmCVec}|\mathrm{IndMet}\left({u}\right)\in \mathrm{CMet}\left(\mathrm{BaseSet}\left({u}\right)\right)\right\}$
12 0 11 wceq ${wff}\mathrm{CBan}=\left\{{u}\in \mathrm{NrmCVec}|\mathrm{IndMet}\left({u}\right)\in \mathrm{CMet}\left(\mathrm{BaseSet}\left({u}\right)\right)\right\}$