Metamath Proof Explorer


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 1A

Proof

Step Hyp Ref Expression
1 elfznn a1Aa
2 1 ssriv 1A