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 )

Proof

Step Hyp Ref Expression
1 df-ds 
 |-  dist = Slot ; 1 2
2 1nn0 
 |-  1 e. NN0
3 2nn 
 |-  2 e. NN
4 2 3 decnncl 
 |-  ; 1 2 e. NN
5 1 4 ndxid 
 |-  dist = Slot ( dist ` ndx )