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 = \{u \in NrmCVec \| IndMet (u) \in CMet (BaseSet (u))\}$

Step	Hyp	Ref	Expression
0		ccbn	$class CBan$
1		vu	$setvar u$
2		cnv	$class NrmCVec$
3		cims	$class IndMet$
4	1	cv	$setvar u$
5	4 3	cfv	$class IndMet (u)$
6		ccmet	$class CMet$
7		cba	$class BaseSet$
8	4 7	cfv	$class BaseSet (u)$
9	8 6	cfv	$class CMet (BaseSet (u))$
10	5 9	wcel	$wff IndMet (u) \in CMet (BaseSet (u))$
11	10 1 2	crab	$class \{u \in NrmCVec \| IndMet (u) \in CMet (BaseSet (u))\}$
12	0 11	wceq	$wff CBan = \{u \in NrmCVec \| IndMet (u) \in CMet (BaseSet (u))\}$

Metamath Proof Explorer