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

Metamath Proof Explorer

Definition df-vr1

Description: Define the base element of a univariate power series (the X element of the set R [ X ] of polynomials and also the X in the set R [ [ X ] ] of power series). (Contributed by Mario Carneiro, 8-Feb-2015)

		Ref	Expression
	Assertion	df-vr1	$⊢ {var}_{1} = (r \in V ⟼ (1_{𝑜} mVar r) (\emptyset))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cv1	$class {var}_{1}$
1		vr	$setvar r$
2		cvv	$class V$
3		c1o	$class 1_{𝑜}$
4		cmvr	$class mVar$
5	1	cv	$setvar r$
6	3 5 4	co	$class (1_{𝑜} mVar r)$
7		c0	$class \emptyset$
8	7 6	cfv	$class (1_{𝑜} mVar r) (\emptyset)$
9	1 2 8	cmpt	$class (r \in V ⟼ (1_{𝑜} mVar r) (\emptyset))$
10	0 9	wceq	$wff {var}_{1} = (r \in V ⟼ (1_{𝑜} mVar r) (\emptyset))$