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

Metamath Proof Explorer

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 ∈ V → ef ⁡ G = G ⁡ ef ⁡ ndx

Proof

Step Hyp Ref Expression
1 edgfid ⊢ ef = Slot ef ⁡ ndx
2 id ⊢ G ∈ V → G ∈ V
3 1 2 strfvnd ⊢ G ∈ V → ef ⁡ G = G ⁡ ef ⁡ ndx