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=WordC∪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→WordmCN⁡t∪mVR⁡t=WordC∪V
11 9 10 syl ⊢t=T→WordmCN⁡t∪mVR⁡t=WordC∪V
12 df-mrex ⊢mREx=t∈V⟼WordmCN⁡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 ⊢WordmCN⁡t∪mVR⁡t∈V
17 11 12 16 fvmpt3i ⊢T∈V→mREx⁡T=WordC∪V
18 4 17 syl ⊢T∈W→mREx⁡T=WordC∪V
19 3 18 eqtrid ⊢T∈W→R=WordC∪V