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.1	$$⊢E=\mathrm{Slot}N$$
	ndxarg.2	$$⊢N\in \mathbb{N}$$
Assertion	ndxarg	$$⊢E\left(\mathrm{ndx}\right)=N$$

Proof

Step	Hyp	Ref	Expression
1		ndxarg.1	$$⊢E=\mathrm{Slot}N$$
2		ndxarg.2	$$⊢N\in \mathbb{N}$$
3		df-ndx	$$⊢\mathrm{ndx}={\mathrm{I}\upharpoonright }_{\mathbb{N}}$$
4		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
5		resiexg	$$⊢\mathbb{N}\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_{\mathbb{N}}\in \mathrm{V}$$
6	4 5	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_{\mathbb{N}}\in \mathrm{V}$$
7	3 6	eqeltri	$$⊢\mathrm{ndx}\in \mathrm{V}$$
8	7 1	strfvn	$$⊢E\left(\mathrm{ndx}\right)=\mathrm{ndx}\left(N\right)$$
9	3	fveq1i	$$⊢\mathrm{ndx}\left(N\right)=\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)\left(N\right)$$
10		fvresi	$$⊢N\in \mathbb{N}\to \left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)\left(N\right)=N$$
11	2 10	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)\left(N\right)=N$$
12	8 9 11	3eqtri	$$⊢E\left(\mathrm{ndx}\right)=N$$