Metamath Proof Explorer

Definition 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 ∈ NrmCVec | IndMet ⁡ u ∈ CMet ⁡ BaseSet ⁡ u

Detailed syntax breakdown

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 ∈ CMet ⁡ BaseSet ⁡ u
11 10 1 2 crab class u ∈ NrmCVec | IndMet ⁡ u ∈ CMet ⁡ BaseSet ⁡ u
12 0 11 wceq wff CBan = u ∈ NrmCVec | IndMet ⁡ u ∈ CMet ⁡ BaseSet ⁡ u