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)

Ref Expression
Assertion edgfndxid 
|- ( G e. V -> ( .ef ` G ) = ( G ` ( .ef ` ndx ) ) )

Proof

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 ) ) )