Metamath Proof Explorer

Theorem edgfndx

Description: Index value of the df-edgf slot. (Contributed by AV, 13-Oct-2024) (New usage is discouraged.)

Ref Expression
Assertion edgfndx 
|- ( .ef ` ndx ) = ; 1 8

Proof

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