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 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-vsca | ⊢ ·𝑠 = Slot 6 | |
| 2 | 6nn | ⊢ 6 ∈ ℕ | |
| 3 | 1 2 | ndxarg | ⊢ ( ·𝑠 ‘ ndx ) = 6 |