Definition df-mvrs

Description: Define the set of variables in an expression. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-mvrs	|- mVars = ( t e. _V |-> ( e e. ( mEx ` t ) |-> ( ran ( 2nd ` e ) i^i ( mVR ` t ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmvrs	|- mVars
1		vt	|- t
2		cvv	|- _V
3		ve	|- e
4		cmex	|- mEx
5	1	cv	|- t
6	5 4	cfv	|- ( mEx ` t )
7		c2nd	|- 2nd
8	3	cv	|- e
9	8 7	cfv	|- ( 2nd ` e )
10	9	crn	|- ran ( 2nd ` e )
11		cmvar	|- mVR
12	5 11	cfv	|- ( mVR ` t )
13	10 12	cin	|- ( ran ( 2nd ` e ) i^i ( mVR ` t ) )
14	3 6 13	cmpt	|- ( e e. ( mEx ` t ) |-> ( ran ( 2nd ` e ) i^i ( mVR ` t ) ) )
15	1 2 14	cmpt	|- ( t e. _V |-> ( e e. ( mEx ` t ) |-> ( ran ( 2nd ` e ) i^i ( mVR ` t ) ) ) )
16	0 15	wceq	|- mVars = ( t e. _V |-> ( e e. ( mEx ` t ) |-> ( ran ( 2nd ` e ) i^i ( mVR ` t ) ) ) )