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

Definition df-mvrs 34147
Description: Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mvrs mVars = (𝑑 ∈ V ↦ (𝑒 ∈ (mExβ€˜π‘‘) ↦ (ran (2nd β€˜π‘’) ∩ (mVRβ€˜π‘‘))))
Distinct variable group:   𝑑,𝑒

Detailed syntax breakdown of Definition df-mvrs
StepHypRef Expression
1 cmvrs 34127 . 2 class mVars
2 vt . . 3 setvar 𝑑
3 cvv 3447 . . 3 class V
4 ve . . . 4 setvar 𝑒
52cv 1541 . . . . 5 class 𝑑
6 cmex 34125 . . . . 5 class mEx
75, 6cfv 6500 . . . 4 class (mExβ€˜π‘‘)
84cv 1541 . . . . . . 7 class 𝑒
9 c2nd 7924 . . . . . . 7 class 2nd
108, 9cfv 6500 . . . . . 6 class (2nd β€˜π‘’)
1110crn 5638 . . . . 5 class ran (2nd β€˜π‘’)
12 cmvar 34119 . . . . . 6 class mVR
135, 12cfv 6500 . . . . 5 class (mVRβ€˜π‘‘)
1411, 13cin 3913 . . . 4 class (ran (2nd β€˜π‘’) ∩ (mVRβ€˜π‘‘))
154, 7, 14cmpt 5192 . . 3 class (𝑒 ∈ (mExβ€˜π‘‘) ↦ (ran (2nd β€˜π‘’) ∩ (mVRβ€˜π‘‘)))
162, 3, 15cmpt 5192 . 2 class (𝑑 ∈ V ↦ (𝑒 ∈ (mExβ€˜π‘‘) ↦ (ran (2nd β€˜π‘’) ∩ (mVRβ€˜π‘‘))))
171, 16wceq 1542 1 wff mVars = (𝑑 ∈ V ↦ (𝑒 ∈ (mExβ€˜π‘‘) ↦ (ran (2nd β€˜π‘’) ∩ (mVRβ€˜π‘‘))))
Colors of variables: wff setvar class
This definition is referenced by:  mvrsval  34163
  Copyright terms: Public domain W3C validator