Definition df-mvt

Description: Define the set of variable typecodes in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-mvt	⊢ mVT = ( 𝑡 ∈ V ↦ ran ( mType ‘ 𝑡 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmvt	⊢ mVT
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		cmty	⊢ mType
4	1	cv	⊢ 𝑡
5	4 3	cfv	⊢ ( mType ‘ 𝑡 )
6	5	crn	⊢ ran ( mType ‘ 𝑡 )
7	1 2 6	cmpt	⊢ ( 𝑡 ∈ V ↦ ran ( mType ‘ 𝑡 ) )
8	0 7	wceq	⊢ mVT = ( 𝑡 ∈ V ↦ ran ( mType ‘ 𝑡 ) )