Metamath Proof Explorer

Theorem tsetndx

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

Ref Expression
Assertion tsetndx 
|- ( TopSet ` ndx ) = 9

Proof

Step Hyp Ref Expression
1 df-tset 
 |-  TopSet = Slot 9
2 9nn 
 |-  9 e. NN
3 1 2 ndxarg 
 |-  ( TopSet ` ndx ) = 9