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	⊢ var1 = ( 𝑟 ∈ V ↦ ( ( 1o mVar 𝑟 ) ‘ ∅ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cv1	⊢ var1
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		c1o	⊢ 1o
4		cmvr	⊢ mVar
5	1	cv	⊢ 𝑟
6	3 5 4	co	⊢ ( 1o mVar 𝑟 )
7		c0	⊢ ∅
8	7 6	cfv	⊢ ( ( 1o mVar 𝑟 ) ‘ ∅ )
9	1 2 8	cmpt	⊢ ( 𝑟 ∈ V ↦ ( ( 1o mVar 𝑟 ) ‘ ∅ ) )
10	0 9	wceq	⊢ var1 = ( 𝑟 ∈ V ↦ ( ( 1o mVar 𝑟 ) ‘ ∅ ) )