Metamath Proof Explorer

Theorem ipndx

Description: Index value of the df-ip slot. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion ipndx 
|- ( .i ` ndx ) = 8

Proof

Step Hyp Ref Expression
1 df-ip 
 |-  .i = Slot 8
2 8nn 
 |-  8 e. NN
3 1 2 ndxarg 
 |-  ( .i ` ndx ) = 8