Theorem ndxarg

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.e	|- E = Slot N
	ndxarg.n	|- N e. NN
Assertion	ndxarg	|- ( E ` ndx ) = N

Proof

Step	Hyp	Ref	Expression
1		ndxarg.e	|- E = Slot N
2		ndxarg.n	|- 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