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

Metamath Proof Explorer

Theorem starvid

Description: Utility theorem: index-independent form of df-starv . (Contributed by Mario Carneiro, 6-Oct-2013)

Ref Expression
Assertion starvid *𝑟 = Slot ( *𝑟 ‘ ndx )

Proof

Step Hyp Ref Expression
1 df-starv ⊢ *𝑟 = Slot 4
2 4nn ⊢ 4 ∈ ℕ
3 1 2 ndxid ⊢ *𝑟 = Slot ( *𝑟 ‘ ndx )