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 )