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

Metamath Proof Explorer

Theorem edgfid

Description: Utility theorem: index-independent form of df-edgf . (Contributed by AV, 16-Nov-2021)

		Ref	Expression
	Assertion	edgfid	$⊢ ef = Slot ef (ndx)$

Step	Hyp	Ref	Expression
1		df-edgf	$⊢ ef = Slot 18$
2		1nn0	$⊢ 1 \in ℕ_{0}$
3		8nn	$⊢ 8 \in ℕ$
4	2 3	decnncl	$⊢ 18 \in ℕ$
5	1 4	ndxid	$⊢ ef = Slot ef (ndx)$