Metamath Proof Explorer

Theorem itvid

Description: Utility theorem: index-independent form of df-itv . (Contributed by Thierry Arnoux, 24-Aug-2017)

Ref Expression
Assertion itvid 
|- Itv = Slot ( Itv ` ndx )

Proof

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