Metamath Proof Explorer


Theorem vscandx

Description: Index value of the df-vsca slot. (Contributed by Mario Carneiro, 14-Aug-2015) (New usage is discouraged.)

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