Definition df-mvrs 35495

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

Step	Hyp	Ref	Expression
1		cmvrs 35475	. 2 class mVars
2		vt	. . 3 setvar 𝑡
3		cvv 3479	. . 3 class V
4		ve	. . . 4 setvar 𝑒
5	2	cv 1538	. . . . 5 class 𝑡
6		cmex 35473	. . . . 5 class mEx
7	5, 6	cfv 6560	. . . 4 class (mEx‘𝑡)
8	4	cv 1538	. . . . . . 7 class 𝑒
9		c2nd 8014	. . . . . . 7 class 2nd
10	8, 9	cfv 6560	. . . . . 6 class (2nd ‘𝑒)
11	10	crn 5685	. . . . 5 class ran (2nd ‘𝑒)
12		cmvar 35467	. . . . . 6 class mVR
13	5, 12	cfv 6560	. . . . 5 class (mVR‘𝑡)
14	11, 13	cin 3949	. . . 4 class (ran (2nd ‘𝑒) ∩ (mVR‘𝑡))
15	4, 7, 14	cmpt 5224	. . 3 class (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd ‘𝑒) ∩ (mVR‘𝑡)))
16	2, 3, 15	cmpt 5224	. 2 class (𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd ‘𝑒) ∩ (mVR‘𝑡))))
17	1, 16	wceq 1539	1 wff mVars = (𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd ‘𝑒) ∩ (mVR‘𝑡))))

This definition is referenced by:  mvrsval  35511