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 = { 𝑢 ∈ NrmCVec ∣ ( IndMet ‘ 𝑢 ) ∈ ( CMet ‘ ( BaseSet ‘ 𝑢 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccbn	⊢ CBan
1		vu	⊢ 𝑢
2		cnv	⊢ NrmCVec
3		cims	⊢ IndMet
4	1	cv	⊢ 𝑢
5	4 3	cfv	⊢ ( IndMet ‘ 𝑢 )
6		ccmet	⊢ CMet
7		cba	⊢ BaseSet
8	4 7	cfv	⊢ ( BaseSet ‘ 𝑢 )
9	8 6	cfv	⊢ ( CMet ‘ ( BaseSet ‘ 𝑢 ) )
10	5 9	wcel	⊢ ( IndMet ‘ 𝑢 ) ∈ ( CMet ‘ ( BaseSet ‘ 𝑢 ) )
11	10 1 2	crab	⊢ { 𝑢 ∈ NrmCVec ∣ ( IndMet ‘ 𝑢 ) ∈ ( CMet ‘ ( BaseSet ‘ 𝑢 ) ) }
12	0 11	wceq	⊢ CBan = { 𝑢 ∈ NrmCVec ∣ ( IndMet ‘ 𝑢 ) ∈ ( CMet ‘ ( BaseSet ‘ 𝑢 ) ) }