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	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	strndxid.e	⊢ 𝐸 = Slot 𝑁
	strndxid.n	⊢ 𝑁 ∈ ℕ
Assertion	strndxid	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐸 ‘ ndx ) ) = ( 𝐸 ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		strndxid.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
2		strndxid.e	⊢ 𝐸 = Slot 𝑁
3		strndxid.n	⊢ 𝑁 ∈ ℕ
4	2 3	ndxid	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
5	4 1	strfvnd	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑆 ) = ( 𝑆 ‘ ( 𝐸 ‘ ndx ) ) )
6	5	eqcomd	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐸 ‘ ndx ) ) = ( 𝐸 ‘ 𝑆 ) )