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