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

Definition df-msub 30177
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  =  ( t  e.  _V  |->  ( f  e.  ( (mREx `  t )  ^pm  (mVR `  t ) )  |->  ( e  e.  (mEx `  t )  |->  <. ( 1st `  e ) ,  ( ( (mRSubst `  t
) `  f ) `  ( 2nd `  e
) ) >. )
) )
Distinct variable group:    e, f, t

Detailed syntax breakdown of Definition df-msub
StepHypRef Expression
1 cmsub 30157 . 2  class mSubst
2 vt . . 3  setvar  t
3 cvv 3056 . . 3  class  _V
4 vf . . . 4  setvar  f
52cv 1453 . . . . . 6  class  t
6 cmrex 30152 . . . . . 6  class mREx
75, 6cfv 5600 . . . . 5  class  (mREx `  t )
8 cmvar 30147 . . . . . 6  class mVR
95, 8cfv 5600 . . . . 5  class  (mVR `  t )
10 cpm 7498 . . . . 5  class  ^pm
117, 9, 10co 6314 . . . 4  class  ( (mREx `  t )  ^pm  (mVR `  t ) )
12 ve . . . . 5  setvar  e
13 cmex 30153 . . . . . 6  class mEx
145, 13cfv 5600 . . . . 5  class  (mEx `  t )
1512cv 1453 . . . . . . 7  class  e
16 c1st 6817 . . . . . . 7  class  1st
1715, 16cfv 5600 . . . . . 6  class  ( 1st `  e )
18 c2nd 6818 . . . . . . . 8  class  2nd
1915, 18cfv 5600 . . . . . . 7  class  ( 2nd `  e )
204cv 1453 . . . . . . . 8  class  f
21 cmrsub 30156 . . . . . . . . 9  class mRSubst
225, 21cfv 5600 . . . . . . . 8  class  (mRSubst `  t
)
2320, 22cfv 5600 . . . . . . 7  class  ( (mRSubst `  t ) `  f
)
2419, 23cfv 5600 . . . . . 6  class  ( ( (mRSubst `  t ) `  f ) `  ( 2nd `  e ) )
2517, 24cop 3985 . . . . 5  class  <. ( 1st `  e ) ,  ( ( (mRSubst `  t
) `  f ) `  ( 2nd `  e
) ) >.
2612, 14, 25cmpt 4474 . . . 4  class  ( e  e.  (mEx `  t
)  |->  <. ( 1st `  e
) ,  ( ( (mRSubst `  t ) `  f ) `  ( 2nd `  e ) )
>. )
274, 11, 26cmpt 4474 . . 3  class  ( f  e.  ( (mREx `  t )  ^pm  (mVR `  t ) )  |->  ( e  e.  (mEx `  t )  |->  <. ( 1st `  e ) ,  ( ( (mRSubst `  t
) `  f ) `  ( 2nd `  e
) ) >. )
)
282, 3, 27cmpt 4474 . 2  class  ( t  e.  _V  |->  ( f  e.  ( (mREx `  t )  ^pm  (mVR `  t ) )  |->  ( e  e.  (mEx `  t )  |->  <. ( 1st `  e ) ,  ( ( (mRSubst `  t
) `  f ) `  ( 2nd `  e
) ) >. )
) )
291, 28wceq 1454 1  wff mSubst  =  ( t  e.  _V  |->  ( f  e.  ( (mREx `  t )  ^pm  (mVR `  t ) )  |->  ( e  e.  (mEx `  t )  |->  <. ( 1st `  e ) ,  ( ( (mRSubst `  t
) `  f ) `  ( 2nd `  e
) ) >. )
) )
Colors of variables: wff setvar class
This definition is referenced by:  msubffval  30209
  Copyright terms: Public domain W3C validator