Metamath Proof Explorer

Theorem unifndx

Description: Index value of the df-unif slot. (Contributed by Thierry Arnoux, 17-Dec-2017) (New usage is discouraged.)

Ref Expression
Assertion unifndx 
|- ( UnifSet ` ndx ) = ; 1 3

Proof

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