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	⊢ N ∈ V

Proof

Step	Hyp	Ref	Expression
1		omex	⊢ ω ∈ V
2		df-ni	⊢ N = ( ω ∖ { ∅ } )
3		difss	⊢ ( ω ∖ { ∅ } ) ⊆ ω
4	2 3	eqsstri	⊢ N ⊆ ω
5	1 4	ssexi	⊢ N ∈ V