This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dsid

Description: Utility theorem: index-independent form of df-ds . (Contributed by Mario Carneiro, 23-Dec-2013)

		Ref	Expression
	Assertion	dsid	$⊢ dist = Slot dist (ndx)$

Step	Hyp	Ref	Expression
1		df-ds	$⊢ dist = Slot 12$
2		1nn0	$⊢ 1 \in ℕ_{0}$
3		2nn	$⊢ 2 \in ℕ$
4	2 3	decnncl	$⊢ 12 \in ℕ$
5	1 4	ndxid	$⊢ dist = Slot dist (ndx)$