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 31149
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 31129 . 2 class mSubst
2 vt . . 3 setvar 𝑡
3 cvv 3190 . . 3 class V
4 vf . . . 4 setvar 𝑓
52cv 1479 . . . . . 6 class 𝑡
6 cmrex 31124 . . . . . 6 class mREx
75, 6cfv 5857 . . . . 5 class (mREx‘𝑡)
8 cmvar 31119 . . . . . 6 class mVR
95, 8cfv 5857 . . . . 5 class (mVR‘𝑡)
10 cpm 7818 . . . . 5 class pm
117, 9, 10co 6615 . . . 4 class ((mREx‘𝑡) ↑pm (mVR‘𝑡))
12 ve . . . . 5 setvar 𝑒
13 cmex 31125 . . . . . 6 class mEx
145, 13cfv 5857 . . . . 5 class (mEx‘𝑡)
1512cv 1479 . . . . . . 7 class 𝑒
16 c1st 7126 . . . . . . 7 class 1st
1715, 16cfv 5857 . . . . . 6 class (1st𝑒)
18 c2nd 7127 . . . . . . . 8 class 2nd
1915, 18cfv 5857 . . . . . . 7 class (2nd𝑒)
204cv 1479 . . . . . . . 8 class 𝑓
21 cmrsub 31128 . . . . . . . . 9 class mRSubst
225, 21cfv 5857 . . . . . . . 8 class (mRSubst‘𝑡)
2320, 22cfv 5857 . . . . . . 7 class ((mRSubst‘𝑡)‘𝑓)
2419, 23cfv 5857 . . . . . 6 class (((mRSubst‘𝑡)‘𝑓)‘(2nd𝑒))
2517, 24cop 4161 . . . . 5 class ⟨(1st𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd𝑒))⟩
2612, 14, 25cmpt 4683 . . . 4 class (𝑒 ∈ (mEx‘𝑡) ↦ ⟨(1st𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd𝑒))⟩)
274, 11, 26cmpt 4683 . . 3 class (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mEx‘𝑡) ↦ ⟨(1st𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd𝑒))⟩))
282, 3, 27cmpt 4683 . 2 class (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mEx‘𝑡) ↦ ⟨(1st𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd𝑒))⟩)))
291, 28wceq 1480 1 wff mSubst = (𝑡 ∈ V ↦ (𝑓 ∈ ((mREx‘𝑡) ↑pm (mVR‘𝑡)) ↦ (𝑒 ∈ (mEx‘𝑡) ↦ ⟨(1st𝑒), (((mRSubst‘𝑡)‘𝑓)‘(2nd𝑒))⟩)))
Colors of variables: wff setvar class
This definition is referenced by:  msubffval  31181
  Copyright terms: Public domain W3C validator