Metamath Proof Explorer

Definition df-edgf

Description: Define the edge function (indexed edges) of a graph. (Contributed by AV, 18-Jan-2020)

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