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	|- CBan = { u e. NrmCVec | ( IndMet ` u ) e. ( CMet ` ( BaseSet ` u ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccbn	|- CBan
1		vu	|- u
2		cnv	|- NrmCVec
3		cims	|- IndMet
4	1	cv	|- u
5	4 3	cfv	|- ( IndMet ` u )
6		ccmet	|- CMet
7		cba	|- BaseSet
8	4 7	cfv	|- ( BaseSet ` u )
9	8 6	cfv	|- ( CMet ` ( BaseSet ` u ) )
10	5 9	wcel	|- ( IndMet ` u ) e. ( CMet ` ( BaseSet ` u ) )
11	10 1 2	crab	|- { u e. NrmCVec | ( IndMet ` u ) e. ( CMet ` ( BaseSet ` u ) ) }
12	0 11	wceq	|- CBan = { u e. NrmCVec | ( IndMet ` u ) e. ( CMet ` ( BaseSet ` u ) ) }