Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Metamath formal systems
mvtval
Next ⟩
mrexval
Metamath Proof Explorer
Ascii
Unicode
Theorem
mvtval
Description:
The set of variable typecodes.
(Contributed by
Mario Carneiro
, 18-Jul-2016)
Ref
Expression
Hypotheses
mvtval.f
⊢
V
=
mVT
⁡
T
mvtval.y
⊢
Y
=
mType
⁡
T
Assertion
mvtval
⊢
V
=
ran
⁡
Y
Proof
Step
Hyp
Ref
Expression
1
mvtval.f
⊢
V
=
mVT
⁡
T
2
mvtval.y
⊢
Y
=
mType
⁡
T
3
fveq2
⊢
t
=
T
→
mType
⁡
t
=
mType
⁡
T
4
3
rneqd
⊢
t
=
T
→
ran
⁡
mType
⁡
t
=
ran
⁡
mType
⁡
T
5
df-mvt
⊢
mVT
=
t
∈
V
⟼
ran
⁡
mType
⁡
t
6
fvex
⊢
mType
⁡
T
∈
V
7
6
rnex
⊢
ran
⁡
mType
⁡
T
∈
V
8
4
5
7
fvmpt
⊢
T
∈
V
→
mVT
⁡
T
=
ran
⁡
mType
⁡
T
9
rn0
⊢
ran
⁡
∅
=
∅
10
9
eqcomi
⊢
∅
=
ran
⁡
∅
11
fvprc
⊢
¬
T
∈
V
→
mVT
⁡
T
=
∅
12
fvprc
⊢
¬
T
∈
V
→
mType
⁡
T
=
∅
13
12
rneqd
⊢
¬
T
∈
V
→
ran
⁡
mType
⁡
T
=
ran
⁡
∅
14
10
11
13
3eqtr4a
⊢
¬
T
∈
V
→
mVT
⁡
T
=
ran
⁡
mType
⁡
T
15
8
14
pm2.61i
⊢
mVT
⁡
T
=
ran
⁡
mType
⁡
T
16
2
rneqi
⊢
ran
⁡
Y
=
ran
⁡
mType
⁡
T
17
15
1
16
3eqtr4i
⊢
V
=
ran
⁡
Y