Metamath Proof Explorer


Definition df-edgf

Description: Define the edge function (indexed edges) of a graph. (Contributed by AV, 18-Jan-2020) Use its index-independent form edgfid instead. (New usage is discouraged.)

Ref Expression
Assertion df-edgf .ef = Slot 1 8

Detailed syntax breakdown

Step Hyp Ref Expression
0 cedgf .ef
1 c1 1
2 c8 8
3 1 2 cdc 1 8
4 3 cslot Slot 1 8
5 0 4 wceq .ef = Slot 1 8