Definition df-mvrs

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

	Ref	Expression
Assertion	df-mvrs	$$⊢\mathrm{mVars}=\left(t\in \mathrm{V}⟼\left(e\in \mathrm{mEx}\left(t\right)⟼\mathrm{ran}{2}^{nd}\left(e\right)\cap \mathrm{mVR}\left(t\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmvrs	$$class\mathrm{mVars}$$
1		vt	$$setvart$$
2		cvv	$$class\mathrm{V}$$
3		ve	$$setvare$$
4		cmex	$$class\mathrm{mEx}$$
5	1	cv	$$setvart$$
6	5 4	cfv	$$class\mathrm{mEx}\left(t\right)$$
7		c2nd	$$class{2}^{nd}$$
8	3	cv	$$setvare$$
9	8 7	cfv	$$class{2}^{nd}\left(e\right)$$
10	9	crn	$$class\mathrm{ran}{2}^{nd}\left(e\right)$$
11		cmvar	$$class\mathrm{mVR}$$
12	5 11	cfv	$$class\mathrm{mVR}\left(t\right)$$
13	10 12	cin	$$class\left(\mathrm{ran}{2}^{nd}\left(e\right)\cap \mathrm{mVR}\left(t\right)\right)$$
14	3 6 13	cmpt	$$class\left(e\in \mathrm{mEx}\left(t\right)⟼\mathrm{ran}{2}^{nd}\left(e\right)\cap \mathrm{mVR}\left(t\right)\right)$$
15	1 2 14	cmpt	$$class\left(t\in \mathrm{V}⟼\left(e\in \mathrm{mEx}\left(t\right)⟼\mathrm{ran}{2}^{nd}\left(e\right)\cap \mathrm{mVR}\left(t\right)\right)\right)$$
16	0 15	wceq	$$wff\mathrm{mVars}=\left(t\in \mathrm{V}⟼\left(e\in \mathrm{mEx}\left(t\right)⟼\mathrm{ran}{2}^{nd}\left(e\right)\cap \mathrm{mVR}\left(t\right)\right)\right)$$