This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ ℕ
Assertion ndxarg ⊢ E ⁡ ndx = N

Proof

Step Hyp Ref Expression
1 ndxarg.e ⊢ E = Slot N
2 ndxarg.n ⊢ N ∈ ℕ
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 ⊢ E ⁡ ndx = ndx ⁡ N
9 3 fveq1i ⊢ ndx ⁡ N = I ↾ ℕ ⁡ N
10 fvresi ⊢ N ∈ ℕ → I ↾ ℕ ⁡ N = N
11 2 10 ax-mp ⊢ I ↾ ℕ ⁡ N = N
12 8 9 11 3eqtri ⊢ E ⁡ ndx = N