Description: Utility theorem: index-independent form of df-starv . (Contributed by Mario Carneiro, 6-Oct-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | starvid | |- *r = Slot ( *r ` ndx ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-starv | |- *r = Slot 4 |
|
2 | 4nn | |- 4 e. NN |
|
3 | 1 2 | ndxid | |- *r = Slot ( *r ` ndx ) |