Metamath Proof Explorer


Theorem mvrcl2

Description: A power series variable is an element of the base set. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses mvrf.s S = I mPwSer R
mvrf.v V = I mVar R
mvrf.b B = Base S
mvrf.i φ I W
mvrf.r φ R Ring
mvrcl2.x φ X I
Assertion mvrcl2 φ V X B

Proof

Step Hyp Ref Expression
1 mvrf.s S = I mPwSer R
2 mvrf.v V = I mVar R
3 mvrf.b B = Base S
4 mvrf.i φ I W
5 mvrf.r φ R Ring
6 mvrcl2.x φ X I
7 1 2 3 4 5 mvrf φ V : I B
8 7 6 ffvelrnd φ V X B