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

Proof

Step	Hyp	Ref	Expression
1		bj-ndxarg.1	|- E = Slot N
2		bj-ndxarg.2	|- N e. NN
3		nnex	|- NN e. _V
4		df-ndx	|- ndx = ( _I |` NN )
5	1 4	fveq12i	|- ( E ` ndx ) = ( Slot N ` ( _I |` NN ) )
6		bj-evalid	|- ( ( NN e. _V /\ N e. NN ) -> ( Slot N ` ( _I |` NN ) ) = N )
7	5 6	syl5eq	|- ( ( NN e. _V /\ N e. NN ) -> ( E ` ndx ) = N )
8	3 2 7	mp2an	|- ( E ` ndx ) = N