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 e. V -> ( .ef ` G ) = ( G ` ( .ef ` ndx ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | edgfid | |- .ef = Slot ( .ef ` ndx ) |
|
| 2 | id | |- ( G e. V -> G e. V ) |
|
| 3 | 1 2 | strfvnd | |- ( G e. V -> ( .ef ` G ) = ( G ` ( .ef ` ndx ) ) ) |