Definition df-bn 8526

Description: Define the class of all complex Banach spaces.

Assertion

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

Detailed syntax breakdown of Definition df-bn

Step	Hyp	Ref	Expression
1		cbn 8525	. 2 class CBan
2		vu	. . . . . 6 set u
3	2	cv 957	. . . . 5 class u
4		cims 8213	. . . . 5 class IndMet
5	3, 4	cfv 3189	. . . 4 class (IndMet` u)
6		cms 7925	. . . 4 class CMet
7	5, 6	wcel 960	. . 3 wff (IndMet` u) e. CMet
8		cnv 8206	. . 3 class NrmCVec
9	7, 2, 8	crab 1651	. 2 class {u e. NrmCVec | (IndMet` u) e. CMet}
10	1, 9	wceq 958	1 wff CBan = {u e. NrmCVec | (IndMet` u) e. CMet}

This definition is referenced by:  isbn 8527

Copyright terms: Public domain