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	⊢ ( 𝐺 ∈ 𝑉 → ( .ef ‘ 𝐺 ) = ( 𝐺 ‘ ( .ef ‘ ndx ) ) )

Proof

Step	Hyp	Ref	Expression
1		edgfid	⊢ .ef = Slot ( .ef ‘ ndx )
2		id	⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ 𝑉 )
3	1 2	strfvnd	⊢ ( 𝐺 ∈ 𝑉 → ( .ef ‘ 𝐺 ) = ( 𝐺 ‘ ( .ef ‘ ndx ) ) )