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

Proof

Step	Hyp	Ref	Expression
1		bj-ndxarg.1	$$⊢E=\mathrm{Slot}N$$
2		bj-ndxarg.2	$$⊢N\in \mathbb{N}$$
3		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
4		df-ndx	$$⊢\mathrm{ndx}={\mathrm{I}\upharpoonright }_{\mathbb{N}}$$
5	1 4	fveq12i	$$⊢E\left(\mathrm{ndx}\right)=\mathrm{Slot}N\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)$$
6		bj-evalid	$$⊢\left(\mathbb{N}\in \mathrm{V}\wedge N\in \mathbb{N}\right)\to \mathrm{Slot}N\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right)=N$$
7	5 6	syl5eq	$$⊢\left(\mathbb{N}\in \mathrm{V}\wedge N\in \mathbb{N}\right)\to E\left(\mathrm{ndx}\right)=N$$
8	3 2 7	mp2an	$$⊢E\left(\mathrm{ndx}\right)=N$$