Theorem ndxid

Description: A structure component extractor is defined by its own index. This theorem, together with strfv below, is useful for avoiding direct reference to the hard-coded numeric index in component extractor definitions, such as the 1 in df-base and the ; 1 0 in df-ple , making it easier to change should the need arise.

For example, we can refer to a specific poset with base set B and order relation L using { <. ( Basendx ) , B >. , <. ( lendx ) , L >. } rather than { <. 1 , B >. , <. ; 1 0 , L >. } . The latter, while shorter to state, requires revision if we later change ; 1 0 to some other number, and it may also be harder to remember. (Contributed by NM, 19-Oct-2012) (Revised by Mario Carneiro, 6-Oct-2013) (Proof shortened by BJ, 27-Dec-2021)

	Ref	Expression
Hypotheses	ndxarg.e	|- E = Slot N
	ndxarg.n	|- N e. NN
Assertion	ndxid	|- E = Slot ( E ` ndx )

Proof

Step	Hyp	Ref	Expression
1		ndxarg.e	|- E = Slot N
2		ndxarg.n	|- N e. NN
3	1 2	ndxarg	|- ( E ` ndx ) = N
4	3	eqcomi	|- N = ( E ` ndx )
5		sloteq	|- ( N = ( E ` ndx ) -> Slot N = Slot ( E ` ndx ) )
6	1 5	eqtrid	|- ( N = ( E ` ndx ) -> E = Slot ( E ` ndx ) )
7	4 6	ax-mp	|- E = Slot ( E ` ndx )