# Metamath Proof Explorer

## Definition df-msub

Description: Define a substitution of expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-msub ${⊢}\mathrm{mSubst}=\left({t}\in \mathrm{V}⟼\left({f}\in \left(\mathrm{mREx}\left({t}\right){↑}_{𝑝𝑚}\mathrm{mVR}\left({t}\right)\right)⟼\left({e}\in \mathrm{mEx}\left({t}\right)⟼⟨{1}^{st}\left({e}\right),\mathrm{mRSubst}\left({t}\right)\left({f}\right)\left({2}^{nd}\left({e}\right)\right)⟩\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cmsub ${class}\mathrm{mSubst}$
1 vt ${setvar}{t}$
2 cvv ${class}\mathrm{V}$
3 vf ${setvar}{f}$
4 cmrex ${class}\mathrm{mREx}$
5 1 cv ${setvar}{t}$
6 5 4 cfv ${class}\mathrm{mREx}\left({t}\right)$
7 cpm ${class}{↑}_{𝑝𝑚}$
8 cmvar ${class}\mathrm{mVR}$
9 5 8 cfv ${class}\mathrm{mVR}\left({t}\right)$
10 6 9 7 co ${class}\left(\mathrm{mREx}\left({t}\right){↑}_{𝑝𝑚}\mathrm{mVR}\left({t}\right)\right)$
11 ve ${setvar}{e}$
12 cmex ${class}\mathrm{mEx}$
13 5 12 cfv ${class}\mathrm{mEx}\left({t}\right)$
14 c1st ${class}{1}^{st}$
15 11 cv ${setvar}{e}$
16 15 14 cfv ${class}{1}^{st}\left({e}\right)$
17 cmrsub ${class}\mathrm{mRSubst}$
18 5 17 cfv ${class}\mathrm{mRSubst}\left({t}\right)$
19 3 cv ${setvar}{f}$
20 19 18 cfv ${class}\mathrm{mRSubst}\left({t}\right)\left({f}\right)$
21 c2nd ${class}{2}^{nd}$
22 15 21 cfv ${class}{2}^{nd}\left({e}\right)$
23 22 20 cfv ${class}\mathrm{mRSubst}\left({t}\right)\left({f}\right)\left({2}^{nd}\left({e}\right)\right)$
24 16 23 cop ${class}⟨{1}^{st}\left({e}\right),\mathrm{mRSubst}\left({t}\right)\left({f}\right)\left({2}^{nd}\left({e}\right)\right)⟩$
25 11 13 24 cmpt ${class}\left({e}\in \mathrm{mEx}\left({t}\right)⟼⟨{1}^{st}\left({e}\right),\mathrm{mRSubst}\left({t}\right)\left({f}\right)\left({2}^{nd}\left({e}\right)\right)⟩\right)$
26 3 10 25 cmpt ${class}\left({f}\in \left(\mathrm{mREx}\left({t}\right){↑}_{𝑝𝑚}\mathrm{mVR}\left({t}\right)\right)⟼\left({e}\in \mathrm{mEx}\left({t}\right)⟼⟨{1}^{st}\left({e}\right),\mathrm{mRSubst}\left({t}\right)\left({f}\right)\left({2}^{nd}\left({e}\right)\right)⟩\right)\right)$
27 1 2 26 cmpt ${class}\left({t}\in \mathrm{V}⟼\left({f}\in \left(\mathrm{mREx}\left({t}\right){↑}_{𝑝𝑚}\mathrm{mVR}\left({t}\right)\right)⟼\left({e}\in \mathrm{mEx}\left({t}\right)⟼⟨{1}^{st}\left({e}\right),\mathrm{mRSubst}\left({t}\right)\left({f}\right)\left({2}^{nd}\left({e}\right)\right)⟩\right)\right)\right)$
28 0 27 wceq ${wff}\mathrm{mSubst}=\left({t}\in \mathrm{V}⟼\left({f}\in \left(\mathrm{mREx}\left({t}\right){↑}_{𝑝𝑚}\mathrm{mVR}\left({t}\right)\right)⟼\left({e}\in \mathrm{mEx}\left({t}\right)⟼⟨{1}^{st}\left({e}\right),\mathrm{mRSubst}\left({t}\right)\left({f}\right)\left({2}^{nd}\left({e}\right)\right)⟩\right)\right)\right)$