Metamath Proof Explorer

Theorem scandx

Description: Index value of the df-sca slot. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion scandx 
|- ( Scalar ` ndx ) = 5

Proof

Step Hyp Ref Expression
1 df-sca 
 |-  Scalar = Slot 5
2 5nn 
 |-  5 e. NN
3 1 2 ndxarg 
 |-  ( Scalar ` ndx ) = 5