Metamath Proof Explorer


Theorem unifid

Description: Utility theorem: index-independent form of df-unif . (Contributed by Thierry Arnoux, 17-Dec-2017)

Ref Expression
Assertion unifid
|- UnifSet = Slot ( UnifSet ` ndx )

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 ndxid
 |-  UnifSet = Slot ( UnifSet ` ndx )