Definition df-deg1

Description: Define the degree of a univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Assertion	df-deg1	$$⊢{\mathrm{deg}}_1=\left(r\in \mathrm{V}⟼1_{𝑜}\mathrm{mDeg}r\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdg1	$$class{\mathrm{deg}}_1$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		c1o	$$class{1}_{𝑜}$$
4		cmdg	$$class\mathrm{mDeg}$$
5	1	cv	$$setvarr$$
6	3 5 4	co	$$class\left(1_{𝑜}\mathrm{mDeg}r\right)$$
7	1 2 6	cmpt	$$class\left(r\in \mathrm{V}⟼1_{𝑜}\mathrm{mDeg}r\right)$$
8	0 7	wceq	$$wff{\mathrm{deg}}_1=\left(r\in \mathrm{V}⟼1_{𝑜}\mathrm{mDeg}r\right)$$