Metamath Proof Explorer


Theorem mrsubffval

Description: The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubffval.c C = mCN T
mrsubffval.v V = mVR T
mrsubffval.r R = mREx T
mrsubffval.s S = mRSubst T
mrsubffval.g G = freeMnd C V
Assertion mrsubffval T W S = f R 𝑝𝑚 V e R G v C V if v dom f f v ⟨“ v ”⟩ e

Proof

Step Hyp Ref Expression
1 mrsubffval.c C = mCN T
2 mrsubffval.v V = mVR T
3 mrsubffval.r R = mREx T
4 mrsubffval.s S = mRSubst T
5 mrsubffval.g G = freeMnd C V
6 elex T W T V
7 fveq2 t = T mREx t = mREx T
8 7 3 syl6eqr t = T mREx t = R
9 fveq2 t = T mVR t = mVR T
10 9 2 syl6eqr t = T mVR t = V
11 8 10 oveq12d t = T mREx t 𝑝𝑚 mVR t = R 𝑝𝑚 V
12 fveq2 t = T mCN t = mCN T
13 12 1 syl6eqr t = T mCN t = C
14 13 10 uneq12d t = T mCN t mVR t = C V
15 14 fveq2d t = T freeMnd mCN t mVR t = freeMnd C V
16 15 5 syl6eqr t = T freeMnd mCN t mVR t = G
17 14 mpteq1d t = T v mCN t mVR t if v dom f f v ⟨“ v ”⟩ = v C V if v dom f f v ⟨“ v ”⟩
18 17 coeq1d t = T v mCN t mVR t if v dom f f v ⟨“ v ”⟩ e = v C V if v dom f f v ⟨“ v ”⟩ e
19 16 18 oveq12d t = T freeMnd mCN t mVR t v mCN t mVR t if v dom f f v ⟨“ v ”⟩ e = G v C V if v dom f f v ⟨“ v ”⟩ e
20 8 19 mpteq12dv t = T e mREx t freeMnd mCN t mVR t v mCN t mVR t if v dom f f v ⟨“ v ”⟩ e = e R G v C V if v dom f f v ⟨“ v ”⟩ e
21 11 20 mpteq12dv t = T f mREx t 𝑝𝑚 mVR t e mREx t freeMnd mCN t mVR t v mCN t mVR t if v dom f f v ⟨“ v ”⟩ e = f R 𝑝𝑚 V e R G v C V if v dom f f v ⟨“ v ”⟩ e
22 df-mrsub mRSubst = t V f mREx t 𝑝𝑚 mVR t e mREx t freeMnd mCN t mVR t v mCN t mVR t if v dom f f v ⟨“ v ”⟩ e
23 ovex R 𝑝𝑚 V V
24 23 mptex f R 𝑝𝑚 V e R G v C V if v dom f f v ⟨“ v ”⟩ e V
25 21 22 24 fvmpt T V mRSubst T = f R 𝑝𝑚 V e R G v C V if v dom f f v ⟨“ v ”⟩ e
26 6 25 syl T W mRSubst T = f R 𝑝𝑚 V e R G v C V if v dom f f v ⟨“ v ”⟩ e
27 4 26 syl5eq T W S = f R 𝑝𝑚 V e R G v C V if v dom f f v ⟨“ v ”⟩ e