Theorem scaid

Description: Utility theorem: index-independent form of scalar df-sca . (Contributed by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Assertion	scaid	⊢ Scalar = Slot ( Scalar ‘ ndx )

Proof

Step	Hyp	Ref	Expression
1		df-sca	⊢ Scalar = Slot 5
2		5nn	⊢ 5 ∈ ℕ
3	1 2	ndxid	⊢ Scalar = Slot ( Scalar ‘ ndx )