Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mvr Structured version   Unicode version

Definition df-mvr 16410
 Description: Define the generating elements of the power series algebra. (Contributed by Mario Carneiro, 7-Jan-2015.)
Assertion
Ref Expression
df-mvr mVar
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-mvr
StepHypRef Expression
1 cmvr 16399 . 2 mVar
2 vi . . 3
3 vr . . 3
4 cvv 2948 . . 3
5 vx . . . 4
62cv 1651 . . . 4
7 vf . . . . 5
8 vh . . . . . . . . . 10
98cv 1651 . . . . . . . . 9
109ccnv 4869 . . . . . . . 8
11 cn 9992 . . . . . . . 8
1210, 11cima 4873 . . . . . . 7
13 cfn 7101 . . . . . . 7
1412, 13wcel 1725 . . . . . 6
15 cn0 10213 . . . . . . 7
16 cmap 7010 . . . . . . 7
1715, 6, 16co 6073 . . . . . 6
1814, 8, 17crab 2701 . . . . 5
197cv 1651 . . . . . . 7
20 vy . . . . . . . 8
2120, 5weq 1653 . . . . . . . . 9
22 c1 8983 . . . . . . . . 9
23 cc0 8982 . . . . . . . . 9
2421, 22, 23cif 3731 . . . . . . . 8
2520, 6, 24cmpt 4258 . . . . . . 7
2619, 25wceq 1652 . . . . . 6
273cv 1651 . . . . . . 7
28 cur 15654 . . . . . . 7
2927, 28cfv 5446 . . . . . 6
30 c0g 13715 . . . . . . 7
3127, 30cfv 5446 . . . . . 6
3226, 29, 31cif 3731 . . . . 5
337, 18, 32cmpt 4258 . . . 4
345, 6, 33cmpt 4258 . . 3
352, 3, 4, 4, 34cmpt2 6075 . 2
361, 35wceq 1652 1 mVar
 Colors of variables: wff set class This definition is referenced by:  mvrfval  16476  vr1val  16582
 Copyright terms: Public domain W3C validator