Theorem bj-ndxarg

Description: Proof of ndxarg from bj-evalid . (Contributed by BJ, 27-Dec-2021) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-ndxarg.1	⊢ 𝐸 = Slot 𝑁
	bj-ndxarg.2	⊢ 𝑁 ∈ ℕ
Assertion	bj-ndxarg	⊢ ( 𝐸 ‘ ndx ) = 𝑁

Proof

Step	Hyp	Ref	Expression
1		bj-ndxarg.1	⊢ 𝐸 = Slot 𝑁
2		bj-ndxarg.2	⊢ 𝑁 ∈ ℕ
3		nnex	⊢ ℕ ∈ V
4		df-ndx	⊢ ndx = ( I ↾ ℕ )
5	1 4	fveq12i	⊢ ( 𝐸 ‘ ndx ) = ( Slot 𝑁 ‘ ( I ↾ ℕ ) )
6		bj-evalid	⊢ ( ( ℕ ∈ V ∧ 𝑁 ∈ ℕ ) → ( Slot 𝑁 ‘ ( I ↾ ℕ ) ) = 𝑁 )
7	5 6	syl5eq	⊢ ( ( ℕ ∈ V ∧ 𝑁 ∈ ℕ ) → ( 𝐸 ‘ ndx ) = 𝑁 )
8	3 2 7	mp2an	⊢ ( 𝐸 ‘ ndx ) = 𝑁