Metamath Proof Explorer


Theorem ccoid

Description: Utility theorem: index-independent form of df-cco . (Contributed by Mario Carneiro, 7-Jan-2017)

Ref Expression
Assertion ccoid comp = Slot comp ndx

Proof

Step Hyp Ref Expression
1 df-cco comp = Slot 15
2 1nn0 1 0
3 5nn 5
4 2 3 decnncl 15
5 1 4 ndxid comp = Slot comp ndx