Theorem edgfndxid

Description: The value of the edge function extractor is the value of the corresponding slot of the structure. (Contributed by AV, 21-Sep-2020) (Proof shortened by AV, 28-Oct-2024)

	Ref	Expression
Assertion	edgfndxid	$$⊢G\in V\to \mathrm{ef}\left(G\right)=G\left(\mathrm{ef}\left(\mathrm{ndx}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		edgfid	$$⊢\mathrm{ef}=\mathrm{Slot}\mathrm{ef}\left(\mathrm{ndx}\right)$$
2		id	$$⊢G\in V\to G\in V$$
3	1 2	strfvnd	$$⊢G\in V\to \mathrm{ef}\left(G\right)=G\left(\mathrm{ef}\left(\mathrm{ndx}\right)\right)$$