Metamath Proof Explorer


Theorem ocid

Description: Utility theorem: index-independent form of df-ocomp . (Contributed by Mario Carneiro, 25-Oct-2015)

Ref Expression
Assertion ocid oc = Slot ( oc ‘ ndx )

Proof

Step Hyp Ref Expression
1 df-ocomp oc = Slot 1 1
2 1nn0 1 ∈ ℕ0
3 1nn 1 ∈ ℕ
4 2 3 decnncl 1 1 ∈ ℕ
5 1 4 ndxid oc = Slot ( oc ‘ ndx )