This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 18$

Detailed syntax breakdown

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