Description: Obsolete version of edgfndxid as of 28-Oct-2024. The value of the edge function extractor is the value of the corresponding slot of the structure. (Contributed by AV, 21-Sep-2020) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | edgfndxidOLD | |- ( G e. V -> ( .ef ` G ) = ( G ` ( .ef ` ndx ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | |- ( G e. V -> G e. V ) |
|
| 2 | df-edgf | |- .ef = Slot ; 1 8 |
|
| 3 | 1nn0 | |- 1 e. NN0 |
|
| 4 | 8nn | |- 8 e. NN |
|
| 5 | 3 4 | decnncl | |- ; 1 8 e. NN |
| 6 | 1 2 5 | strndxid | |- ( G e. V -> ( G ` ( .ef ` ndx ) ) = ( .ef ` G ) ) |
| 7 | 6 | eqcomd | |- ( G e. V -> ( .ef ` G ) = ( G ` ( .ef ` ndx ) ) ) |