Metamath Proof Explorer


Theorem mrexval

Description: The set of "raw expressions", which are expressions without a typecode, that is, just sequences of constants and variables. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrexval.c C = mCN T
mrexval.v V = mVR T
mrexval.r R = mREx T
Assertion mrexval T W R = Word C V

Proof

Step Hyp Ref Expression
1 mrexval.c C = mCN T
2 mrexval.v V = mVR T
3 mrexval.r R = mREx T
4 elex T W T V
5 fveq2 t = T mCN t = mCN T
6 5 1 eqtr4di t = T mCN t = C
7 fveq2 t = T mVR t = mVR T
8 7 2 eqtr4di t = T mVR t = V
9 6 8 uneq12d t = T mCN t mVR t = C V
10 wrdeq mCN t mVR t = C V Word mCN t mVR t = Word C V
11 9 10 syl t = T Word mCN t mVR t = Word C V
12 df-mrex mREx = t V Word mCN t mVR t
13 fvex mCN t V
14 fvex mVR t V
15 13 14 unex mCN t mVR t V
16 15 wrdexi Word mCN t mVR t V
17 11 12 16 fvmpt3i T V mREx T = Word C V
18 4 17 syl T W mREx T = Word C V
19 3 18 syl5eq T W R = Word C V