Metamath Proof Explorer

Theorem lngndx

Description: Index value of the "line" slot. Use ndxarg . (Contributed by Thierry Arnoux, 27-Mar-2019)

Ref Expression
Assertion lngndx 
|- ( LineG ` ndx ) = ; 1 7

Proof

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