Metamath Proof Explorer

Theorem plusgndx

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

Ref Expression
Assertion plusgndx 
|- ( +g ` ndx ) = 2

Proof

Step Hyp Ref Expression
1 df-plusg 
 |-  +g = Slot 2
2 2nn 
 |-  2 e. NN
3 1 2 ndxarg 
 |-  ( +g ` ndx ) = 2