Database
BASIC STRUCTURES
Extensible structures
Slot definitions
vscandx
Next ⟩
vscaid
Metamath Proof Explorer
Ascii
Unicode
Theorem
vscandx
Description:
Index value of the
df-vsca
slot.
(Contributed by
Mario Carneiro
, 14-Aug-2015)
Ref
Expression
Assertion
vscandx
⊢
⋅
ndx
=
6
Proof
Step
Hyp
Ref
Expression
1
df-vsca
⊢
⋅
𝑠
=
Slot
6
2
6nn
⊢
6
∈
ℕ
3
1
2
ndxarg
⊢
⋅
ndx
=
6