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 ∈ ℕ
3	1 2	ndxid	⊢ le = Slot ( le ‘ ndx )