Theorem strndxid

Description: The value of a structure component extractor is the value of the corresponding slot of the structure. (Contributed by AV, 13-Mar-2020)

	Ref	Expression
Hypotheses	strndxid.s	|- ( ph -> S e. V )
	strndxid.e	|- E = Slot N
	strndxid.n	|- N e. NN
Assertion	strndxid	|- ( ph -> ( S ` ( E ` ndx ) ) = ( E ` S ) )

Proof

Step	Hyp	Ref	Expression
1		strndxid.s	|- ( ph -> S e. V )
2		strndxid.e	|- E = Slot N
3		strndxid.n	|- N e. NN
4	2 3	ndxid	|- E = Slot ( E ` ndx )
5	4 1	strfvnd	|- ( ph -> ( E ` S ) = ( S ` ( E ` ndx ) ) )
6	5	eqcomd	|- ( ph -> ( S ` ( E ` ndx ) ) = ( E ` S ) )