Metamath Proof Explorer


Theorem mvtss

Description: The set of variable typecodes is a subset of all typecodes. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mvtss.f F = mVT T
mvtss.k K = mTC T
Assertion mvtss T mFS F K

Proof

Step Hyp Ref Expression
1 mvtss.f F = mVT T
2 mvtss.k K = mTC T
3 eqid mType T = mType T
4 1 3 mvtval F = ran mType T
5 eqid mVR T = mVR T
6 5 2 3 mtyf2 T mFS mType T : mVR T K
7 6 frnd T mFS ran mType T K
8 4 7 eqsstrid T mFS F K