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	⊢ 𝐸 = Slot 𝑁
	ndxarg.2	⊢ 𝑁 ∈ ℕ
Assertion	ndxarg	⊢ ( 𝐸 ‘ ndx ) = 𝑁

Proof

Step	Hyp	Ref	Expression
1		ndxarg.1	⊢ 𝐸 = Slot 𝑁
2		ndxarg.2	⊢ 𝑁 ∈ ℕ
3		df-ndx	⊢ ndx = ( I ↾ ℕ )
4		nnex	⊢ ℕ ∈ V
5		resiexg	⊢ ( ℕ ∈ V → ( I ↾ ℕ ) ∈ V )
6	4 5	ax-mp	⊢ ( I ↾ ℕ ) ∈ V
7	3 6	eqeltri	⊢ ndx ∈ V
8	7 1	strfvn	⊢ ( 𝐸 ‘ ndx ) = ( ndx ‘ 𝑁 )
9	3	fveq1i	⊢ ( ndx ‘ 𝑁 ) = ( ( I ↾ ℕ ) ‘ 𝑁 )
10		fvresi	⊢ ( 𝑁 ∈ ℕ → ( ( I ↾ ℕ ) ‘ 𝑁 ) = 𝑁 )
11	2 10	ax-mp	⊢ ( ( I ↾ ℕ ) ‘ 𝑁 ) = 𝑁
12	8 9 11	3eqtri	⊢ ( 𝐸 ‘ ndx ) = 𝑁