Metamath Proof Explorer

Theorem ipid

Description: Utility theorem: index-independent form of df-ip . (Contributed by Mario Carneiro, 6-Oct-2013)

Ref Expression
Assertion ipid 
|- .i = Slot ( .i ` ndx )

Proof

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