Metamath Proof Explorer

Theorem pleid

Description: Utility theorem: self-referencing, index-independent form of df-ple . (Contributed by NM, 9-Nov-2012) (Revised by AV, 9-Sep-2021)

Ref Expression
Assertion pleid 
|- le = Slot ( le ` ndx )

Proof

Step Hyp Ref Expression
1 df-ple 
 |-  le = Slot ; 1 0
2 10nn 
 |-  ; 1 0 e. NN
3 1 2 ndxid 
 |-  le = Slot ( le ` ndx )