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