Theorem mulridx

Description: Utility theorem: index-independent form of df-mulr . (Contributed by Mario Carneiro, 8-Jun-2013)

	Ref	Expression
Assertion	mulridx	$$⊢{\cdot }_{𝑟}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$

Proof

Step	Hyp	Ref	Expression
1		df-mulr	$$⊢{\cdot }_{𝑟}=\mathrm{Slot}3$$
2		3nn	$$⊢3\in \mathbb{N}$$
3	1 2	ndxid	$$⊢{\cdot }_{𝑟}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$