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 |