Theorem ipid

Description: Utility theorem: index-independent form of df-ip . (Contributed by Mario Carneiro, 6-Oct-2013)

	Ref	Expression
Assertion	ipid	$$⊢{\cdot }_{𝑖}=\mathrm{Slot}{\cdot }_{𝑖}\left(\mathrm{ndx}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ip	$$⊢{\cdot }_{𝑖}=\mathrm{Slot}8$$
2		8nn	$$⊢8\in \mathbb{N}$$
3	1 2	ndxid	$$⊢{\cdot }_{𝑖}=\mathrm{Slot}{\cdot }_{𝑖}\left(\mathrm{ndx}\right)$$