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

Definition df-mvrs 30175
Description: Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mvrs  |- mVars  =  ( t  e.  _V  |->  ( e  e.  (mEx `  t )  |->  ( ran  ( 2nd `  e
)  i^i  (mVR `  t
) ) ) )
Distinct variable group:    t, e

Detailed syntax breakdown of Definition df-mvrs
StepHypRef Expression
1 cmvrs 30155 . 2  class mVars
2 vt . . 3  setvar  t
3 cvv 3056 . . 3  class  _V
4 ve . . . 4  setvar  e
52cv 1453 . . . . 5  class  t
6 cmex 30153 . . . . 5  class mEx
75, 6cfv 5600 . . . 4  class  (mEx `  t )
84cv 1453 . . . . . . 7  class  e
9 c2nd 6818 . . . . . . 7  class  2nd
108, 9cfv 5600 . . . . . 6  class  ( 2nd `  e )
1110crn 4853 . . . . 5  class  ran  ( 2nd `  e )
12 cmvar 30147 . . . . . 6  class mVR
135, 12cfv 5600 . . . . 5  class  (mVR `  t )
1411, 13cin 3414 . . . 4  class  ( ran  ( 2nd `  e
)  i^i  (mVR `  t
) )
154, 7, 14cmpt 4474 . . 3  class  ( e  e.  (mEx `  t
)  |->  ( ran  ( 2nd `  e )  i^i  (mVR `  t )
) )
162, 3, 15cmpt 4474 . 2  class  ( t  e.  _V  |->  ( e  e.  (mEx `  t
)  |->  ( ran  ( 2nd `  e )  i^i  (mVR `  t )
) ) )
171, 16wceq 1454 1  wff mVars  =  ( t  e.  _V  |->  ( e  e.  (mEx `  t )  |->  ( ran  ( 2nd `  e
)  i^i  (mVR `  t
) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  mvrsval  30191
  Copyright terms: Public domain W3C validator