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	$$⊢\phi \to S\in V$$
	strndxid.e	$$⊢E=\mathrm{Slot}N$$
	strndxid.n	$$⊢N\in \mathbb{N}$$
Assertion	strndxid	$$⊢\phi \to S\left(E\left(\mathrm{ndx}\right)\right)=E\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		strndxid.s	$$⊢\phi \to S\in V$$
2		strndxid.e	$$⊢E=\mathrm{Slot}N$$
3		strndxid.n	$$⊢N\in \mathbb{N}$$
4	2 3	ndxid	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
5	4 1	strfvnd	$$⊢\phi \to E\left(S\right)=S\left(E\left(\mathrm{ndx}\right)\right)$$
6	5	eqcomd	$$⊢\phi \to S\left(E\left(\mathrm{ndx}\right)\right)=E\left(S\right)$$