Metamath Proof Explorer


Theorem edgfid

Description: Utility theorem: index-independent form of df-edgf . (Contributed by AV, 16-Nov-2021)

Ref Expression
Assertion edgfid ef = Slot ef ndx

Proof

Step Hyp Ref Expression
1 df-edgf ef = Slot 18
2 1nn0 1 0
3 8nn 8
4 2 3 decnncl 18
5 1 4 ndxid ef = Slot ef ndx