Theorem fz1ssnn

Description: A finite set of positive integers is a set of positive integers. (Contributed by Stefan O'Rear, 16-Oct-2014)

	Ref	Expression
Assertion	fz1ssnn	⊢ ( 1 ... 𝐴 ) ⊆ ℕ

Proof

Step	Hyp	Ref	Expression
1		elfznn	⊢ ( 𝑎 ∈ ( 1 ... 𝐴 ) → 𝑎 ∈ ℕ )
2	1	ssriv	⊢ ( 1 ... 𝐴 ) ⊆ ℕ