Theorem niex

Description: The class of positive integers is a set. (Contributed by NM, 15-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	niex	$$⊢𝑵\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
2		df-ni	$$⊢𝑵=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
3		difss	$$⊢\mathrm{\omega }\setminus \left\{\varnothing \right\}\subseteq \mathrm{\omega }$$
4	2 3	eqsstri	$$⊢𝑵\subseteq \mathrm{\omega }$$
5	1 4	ssexi	$$⊢𝑵\in \mathrm{V}$$