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 ; 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