Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-msub Structured version   Visualization version   GIF version

Definition df-msub 34149
Description: Define a substitution of expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-msub mSubst = (𝑑 ∈ V ↦ (𝑓 ∈ ((mRExβ€˜π‘‘) ↑pm (mVRβ€˜π‘‘)) ↦ (𝑒 ∈ (mExβ€˜π‘‘) ↦ ⟨(1st β€˜π‘’), (((mRSubstβ€˜π‘‘)β€˜π‘“)β€˜(2nd β€˜π‘’))⟩)))
Distinct variable group:   𝑒,𝑓,𝑑

Detailed syntax breakdown of Definition df-msub
StepHypRef Expression
1 cmsub 34129 . 2 class mSubst
2 vt . . 3 setvar 𝑑
3 cvv 3447 . . 3 class V
4 vf . . . 4 setvar 𝑓
52cv 1541 . . . . . 6 class 𝑑
6 cmrex 34124 . . . . . 6 class mREx
75, 6cfv 6500 . . . . 5 class (mRExβ€˜π‘‘)
8 cmvar 34119 . . . . . 6 class mVR
95, 8cfv 6500 . . . . 5 class (mVRβ€˜π‘‘)
10 cpm 8772 . . . . 5 class ↑pm
117, 9, 10co 7361 . . . 4 class ((mRExβ€˜π‘‘) ↑pm (mVRβ€˜π‘‘))
12 ve . . . . 5 setvar 𝑒
13 cmex 34125 . . . . . 6 class mEx
145, 13cfv 6500 . . . . 5 class (mExβ€˜π‘‘)
1512cv 1541 . . . . . . 7 class 𝑒
16 c1st 7923 . . . . . . 7 class 1st
1715, 16cfv 6500 . . . . . 6 class (1st β€˜π‘’)
18 c2nd 7924 . . . . . . . 8 class 2nd
1915, 18cfv 6500 . . . . . . 7 class (2nd β€˜π‘’)
204cv 1541 . . . . . . . 8 class 𝑓
21 cmrsub 34128 . . . . . . . . 9 class mRSubst
225, 21cfv 6500 . . . . . . . 8 class (mRSubstβ€˜π‘‘)
2320, 22cfv 6500 . . . . . . 7 class ((mRSubstβ€˜π‘‘)β€˜π‘“)
2419, 23cfv 6500 . . . . . 6 class (((mRSubstβ€˜π‘‘)β€˜π‘“)β€˜(2nd β€˜π‘’))
2517, 24cop 4596 . . . . 5 class ⟨(1st β€˜π‘’), (((mRSubstβ€˜π‘‘)β€˜π‘“)β€˜(2nd β€˜π‘’))⟩
2612, 14, 25cmpt 5192 . . . 4 class (𝑒 ∈ (mExβ€˜π‘‘) ↦ ⟨(1st β€˜π‘’), (((mRSubstβ€˜π‘‘)β€˜π‘“)β€˜(2nd β€˜π‘’))⟩)
274, 11, 26cmpt 5192 . . 3 class (𝑓 ∈ ((mRExβ€˜π‘‘) ↑pm (mVRβ€˜π‘‘)) ↦ (𝑒 ∈ (mExβ€˜π‘‘) ↦ ⟨(1st β€˜π‘’), (((mRSubstβ€˜π‘‘)β€˜π‘“)β€˜(2nd β€˜π‘’))⟩))
282, 3, 27cmpt 5192 . 2 class (𝑑 ∈ V ↦ (𝑓 ∈ ((mRExβ€˜π‘‘) ↑pm (mVRβ€˜π‘‘)) ↦ (𝑒 ∈ (mExβ€˜π‘‘) ↦ ⟨(1st β€˜π‘’), (((mRSubstβ€˜π‘‘)β€˜π‘“)β€˜(2nd β€˜π‘’))⟩)))
291, 28wceq 1542 1 wff mSubst = (𝑑 ∈ V ↦ (𝑓 ∈ ((mRExβ€˜π‘‘) ↑pm (mVRβ€˜π‘‘)) ↦ (𝑒 ∈ (mExβ€˜π‘‘) ↦ ⟨(1st β€˜π‘’), (((mRSubstβ€˜π‘‘)β€˜π‘“)β€˜(2nd β€˜π‘’))⟩)))
Colors of variables: wff setvar class
This definition is referenced by:  msubffval  34181
  Copyright terms: Public domain W3C validator