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