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 = ( 𝑡 ∈ V ↦ ( 𝑒 ∈ ( mEx ‘ 𝑡 ) ↦ ( ran ( 2nd ‘ 𝑒 ) ∩ ( mVR ‘ 𝑡 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmvrs	⊢ mVars
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		ve	⊢ 𝑒
4		cmex	⊢ mEx
5	1	cv	⊢ 𝑡
6	5 4	cfv	⊢ ( mEx ‘ 𝑡 )
7		c2nd	⊢ 2nd
8	3	cv	⊢ 𝑒
9	8 7	cfv	⊢ ( 2nd ‘ 𝑒 )
10	9	crn	⊢ ran ( 2nd ‘ 𝑒 )
11		cmvar	⊢ mVR
12	5 11	cfv	⊢ ( mVR ‘ 𝑡 )
13	10 12	cin	⊢ ( ran ( 2nd ‘ 𝑒 ) ∩ ( mVR ‘ 𝑡 ) )
14	3 6 13	cmpt	⊢ ( 𝑒 ∈ ( mEx ‘ 𝑡 ) ↦ ( ran ( 2nd ‘ 𝑒 ) ∩ ( mVR ‘ 𝑡 ) ) )
15	1 2 14	cmpt	⊢ ( 𝑡 ∈ V ↦ ( 𝑒 ∈ ( mEx ‘ 𝑡 ) ↦ ( ran ( 2nd ‘ 𝑒 ) ∩ ( mVR ‘ 𝑡 ) ) ) )
16	0 15	wceq	⊢ mVars = ( 𝑡 ∈ V ↦ ( 𝑒 ∈ ( mEx ‘ 𝑡 ) ↦ ( ran ( 2nd ‘ 𝑒 ) ∩ ( mVR ‘ 𝑡 ) ) ) )