Definition df-mvrs 35478

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 35458	. 2 class mVars
2		vt	. . 3 setvar 𝑡
3		cvv 3455	. . 3 class V
4		ve	. . . 4 setvar 𝑒
5	2	cv 1539	. . . . 5 class 𝑡
6		cmex 35456	. . . . 5 class mEx
7	5, 6	cfv 6519	. . . 4 class (mEx‘𝑡)
8	4	cv 1539	. . . . . . 7 class 𝑒
9		c2nd 7976	. . . . . . 7 class 2nd
10	8, 9	cfv 6519	. . . . . 6 class (2nd ‘𝑒)
11	10	crn 5647	. . . . 5 class ran (2nd ‘𝑒)
12		cmvar 35450	. . . . . 6 class mVR
13	5, 12	cfv 6519	. . . . 5 class (mVR‘𝑡)
14	11, 13	cin 3921	. . . 4 class (ran (2nd ‘𝑒) ∩ (mVR‘𝑡))
15	4, 7, 14	cmpt 5196	. . 3 class (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd ‘𝑒) ∩ (mVR‘𝑡)))
16	2, 3, 15	cmpt 5196	. 2 class (𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd ‘𝑒) ∩ (mVR‘𝑡))))
17	1, 16	wceq 1540	1 wff mVars = (𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd ‘𝑒) ∩ (mVR‘𝑡))))

This definition is referenced by:  mvrsval  35494