Definition df-ba

Description: Define the base set of a normed complex vector space. (Contributed by NM, 23-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ba	$$⊢\mathrm{BaseSet}=\left(x\in \mathrm{V}⟼\mathrm{ran}{+}_v\left(x\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cba	$$class\mathrm{BaseSet}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		cpv	$$class{+}_v$$
4	1	cv	$$setvarx$$
5	4 3	cfv	$$class{+}_v\left(x\right)$$
6	5	crn	$$class\mathrm{ran}{+}_v\left(x\right)$$
7	1 2 6	cmpt	$$class\left(x\in \mathrm{V}⟼\mathrm{ran}{+}_v\left(x\right)\right)$$
8	0 7	wceq	$$wff\mathrm{BaseSet}=\left(x\in \mathrm{V}⟼\mathrm{ran}{+}_v\left(x\right)\right)$$