This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ BaseSet = (x \in V ⟼ ran +_{v} (x))$

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