Definition df-cbn 27719

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

Assertion

Ref	Expression
df-cbn	|- CBan = { u e. NrmCVec | ( IndMet ` u ) e. ( CMet ` ( BaseSet ` u ) ) }

Detailed syntax breakdown of Definition df-cbn

Step	Hyp	Ref	Expression
1		ccbn 27718	. 2 class CBan
2		vu	. . . . . 6 setvar u
3	2	cv 1482	. . . . 5 class u
4		cims 27446	. . . . 5 class IndMet
5	3, 4	cfv 5888	. . . 4 class ( IndMet ` u )
6		cba 27441	. . . . . 6 class BaseSet
7	3, 6	cfv 5888	. . . . 5 class ( BaseSet ` u )
8		cms 23052	. . . . 5 class CMet
9	7, 8	cfv 5888	. . . 4 class ( CMet ` ( BaseSet ` u ) )
10	5, 9	wcel 1990	. . 3 wff ( IndMet ` u ) e. ( CMet ` ( BaseSet ` u ) )
11		cnv 27439	. . 3 class NrmCVec
12	10, 2, 11	crab 2916	. 2 class { u e. NrmCVec | ( IndMet ` u ) e. ( CMet ` ( BaseSet ` u ) ) }
13	1, 12	wceq 1483	1 wff CBan = { u e. NrmCVec | ( IndMet ` u ) e. ( CMet ` ( BaseSet ` u ) ) }

This definition is referenced by:  iscbn  27720