Definition df-bn 8523

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 8522	. 2 class CBan
2		vu	. . . . . 6 set u
3	2	cv 955	. . . . 5 class u
4		cims 8210	. . . . 5 class IndMet
5	3, 4	cfv 3182	. . . 4 class (IndMet` u)
6		cms 7921	. . . 4 class CMet
7	5, 6	wcel 958	. . 3 wff (IndMet` u) e. CMet
8		cnv 8203	. . 3 class NrmCVec
9	7, 2, 8	crab 1648	. 2 class {u e. NrmCVec | (IndMet` u) e. CMet}
10	1, 9	wceq 956	1 wff CBan = {u e. NrmCVec | (IndMet` u) e. CMet}

This definition is referenced by:  isbn 8524

Copyright terms: Public domain