Definition df-cbn 29868

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

Assertion

Ref	Expression
df-cbn	⊢ CBan = {𝑢 ∈ NrmCVec ∣ (IndMet‘𝑢) ∈ (CMet‘(BaseSet‘𝑢))}

Detailed syntax breakdown of Definition df-cbn

Step	Hyp	Ref	Expression
1		ccbn 29867	. 2 class CBan
2		vu	. . . . . 6 setvar 𝑢
3	2	cv 1540	. . . . 5 class 𝑢
4		cims 29596	. . . . 5 class IndMet
5	3, 4	cfv 6501	. . . 4 class (IndMet‘𝑢)
6		cba 29591	. . . . . 6 class BaseSet
7	3, 6	cfv 6501	. . . . 5 class (BaseSet‘𝑢)
8		ccmet 24655	. . . . 5 class CMet
9	7, 8	cfv 6501	. . . 4 class (CMet‘(BaseSet‘𝑢))
10	5, 9	wcel 2106	. . 3 wff (IndMet‘𝑢) ∈ (CMet‘(BaseSet‘𝑢))
11		cnv 29589	. . 3 class NrmCVec
12	10, 2, 11	crab 3405	. 2 class {𝑢 ∈ NrmCVec ∣ (IndMet‘𝑢) ∈ (CMet‘(BaseSet‘𝑢))}
13	1, 12	wceq 1541	1 wff CBan = {𝑢 ∈ NrmCVec ∣ (IndMet‘𝑢) ∈ (CMet‘(BaseSet‘𝑢))}

This definition is referenced by:  iscbn  29869