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
|- *r = Slot ( *r ` ndx )

Proof

Step Hyp Ref Expression
1 df-starv
 |-  *r = Slot 4
2 4nn
 |-  4 e. NN
3 1 2 ndxid
 |-  *r = Slot ( *r ` ndx )