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	$$⊢{\mathrm{var}}_1=\left(r\in \mathrm{V}⟼\left(1_{𝑜}\mathrm{mVar}r\right)\left(\varnothing \right)\right)$$

Detailed syntax breakdown

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