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 ⊢ mSubst = t ∈ V ⟼ f ∈ mREx ⁡ t ↑ 𝑝𝑚 mVR ⁡ t ⟼ e ∈ mEx ⁡ t ⟼ 1 st ⁡ e mRSubst ⁡ t ⁡ f ⁡ 2 nd ⁡ e

Detailed syntax breakdown

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