Metamath Proof Explorer

Theorem dsndx

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

Ref Expression
Assertion dsndx 
|- ( dist ` ndx ) = ; 1 2

Proof

Step Hyp Ref Expression
1 df-ds 
 |-  dist = Slot ; 1 2
2 1nn0 
 |-  1 e. NN0
3 2nn 
 |-  2 e. NN
4 2 3 decnncl 
 |-  ; 1 2 e. NN
5 1 4 ndxarg 
 |-  ( dist ` ndx ) = ; 1 2