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