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	$$⊢\mathrm{le}=\mathrm{Slot}{\le }_{\mathrm{ndx}}$$

Proof

Step	Hyp	Ref	Expression
1		df-ple	$$⊢\mathrm{le}=\mathrm{Slot}10$$
2		10nn	$$⊢10\in \mathbb{N}$$
3	1 2	ndxid	$$⊢\mathrm{le}=\mathrm{Slot}{\le }_{\mathrm{ndx}}$$