Theorem mulridx

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

	Ref	Expression
Assertion	mulridx	⊢ .r = Slot ( .r ‘ ndx )

Proof

Step	Hyp	Ref	Expression
1		df-mulr	⊢ .r = Slot 3
2		3nn	⊢ 3 ∈ ℕ
3	1 2	ndxid	⊢ .r = Slot ( .r ‘ ndx )