Definition df-bn 8454

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 8453	. 2 class CBan
2		vu	. . . . . 6 set u
3	2	cv 952	. . . . 5 class u
4		cims 8148	. . . . 5 class IndMet
5	3, 4	cfv 3172	. . . 4 class (IndMet` u)
6		cms 7859	. . . 4 class CMet
7	5, 6	wcel 955	. . 3 wff (IndMet` u) e. CMet
8		cnv 8141	. . 3 class NrmCVec
9	7, 2, 8	crab 1640	. 2 class {u e. NrmCVec | (IndMet` u) e. CMet}
10	1, 9	wceq 953	1 wff CBan = {u e. NrmCVec | (IndMet` u) e. CMet}

This definition is referenced by:  isbn 8455

Copyright terms: Public domain