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 )