# 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 ${⊢}{\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 ${setvar}{r}$
2 cvv ${class}\mathrm{V}$
3 c1o ${class}{1}_{𝑜}$
4 cmvr ${class}\mathrm{mVar}$
5 1 cv ${setvar}{r}$
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)$