This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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) (New usage is discouraged.) Use strfvnd directly with N set to ( Endx ) if possible.

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 ) ) = ( 𝐸 ‘ 𝑆 ) )