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

Step	Hyp	Ref	Expression
1		cmvrs 30155	. 2 class mVars
2		vt	. . 3 setvar t
3		cvv 3056	. . 3 class _V
4		ve	. . . 4 setvar e
5	2	cv 1453	. . . . 5 class t
6		cmex 30153	. . . . 5 class mEx
7	5, 6	cfv 5600	. . . 4 class (mEx ` t )
8	4	cv 1453	. . . . . . 7 class e
9		c2nd 6818	. . . . . . 7 class 2nd
10	8, 9	cfv 5600	. . . . . 6 class ( 2nd ` e )
11	10	crn 4853	. . . . 5 class ran ( 2nd ` e )
12		cmvar 30147	. . . . . 6 class mVR
13	5, 12	cfv 5600	. . . . 5 class (mVR ` t )
14	11, 13	cin 3414	. . . 4 class ( ran ( 2nd ` e ) i^i (mVR ` t ) )
15	4, 7, 14	cmpt 4474	. . 3 class ( e e. (mEx ` t ) |-> ( ran ( 2nd ` e ) i^i (mVR ` t ) ) )
16	2, 3, 15	cmpt 4474	. 2 class ( t e. _V |-> ( e e. (mEx ` t ) |-> ( ran ( 2nd ` e ) i^i (mVR ` t ) ) ) )
17	1, 16	wceq 1454	1 wff mVars = ( t e. _V |-> ( e e. (mEx ` t ) |-> ( ran ( 2nd ` e ) i^i (mVR ` t ) ) ) )

This definition is referenced by:  mvrsval  30191