Theorem ipid

Description: Utility theorem: index-independent form of df-ip . (Contributed by Mario Carneiro, 6-Oct-2013)

	Ref	Expression
Assertion	ipid	⊢ ·𝑖 = Slot ( ·𝑖 ‘ ndx )

Proof

Step	Hyp	Ref	Expression
1		df-ip	⊢ ·𝑖 = Slot 8
2		8nn	⊢ 8 ∈ ℕ
3	1 2	ndxid	⊢ ·𝑖 = Slot ( ·𝑖 ‘ ndx )