Metamath Proof Explorer


Theorem lngid

Description: Utility theorem: index-independent form of df-lng . (Contributed by Thierry Arnoux, 27-Mar-2019)

Ref Expression
Assertion lngid
|- LineG = Slot ( LineG ` ndx )

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 ndxid
 |-  LineG = Slot ( LineG ` ndx )