Description: Get the numeric argument from a defined structure component extractor such as df-base . (Contributed by Mario Carneiro, 6-Oct-2013)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ndxarg.1 | |- E = Slot N |
|
| ndxarg.2 | |- N e. NN |
||
| Assertion | ndxarg | |- ( E ` ndx ) = N |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ndxarg.1 | |- E = Slot N |
|
| 2 | ndxarg.2 | |- N e. NN |
|
| 3 | df-ndx | |- ndx = ( _I |` NN ) |
|
| 4 | nnex | |- NN e. _V |
|
| 5 | resiexg | |- ( NN e. _V -> ( _I |` NN ) e. _V ) |
|
| 6 | 4 5 | ax-mp | |- ( _I |` NN ) e. _V |
| 7 | 3 6 | eqeltri | |- ndx e. _V |
| 8 | 7 1 | strfvn | |- ( E ` ndx ) = ( ndx ` N ) |
| 9 | 3 | fveq1i | |- ( ndx ` N ) = ( ( _I |` NN ) ` N ) |
| 10 | fvresi | |- ( N e. NN -> ( ( _I |` NN ) ` N ) = N ) |
|
| 11 | 2 10 | ax-mp | |- ( ( _I |` NN ) ` N ) = N |
| 12 | 8 9 11 | 3eqtri | |- ( E ` ndx ) = N |