Theorem niex 6438

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

Assertion

Ref	Expression
niex	⊢ N ∈ V

Proof of Theorem niex

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

Syntax hints:   ∈ wcel 1407  Vcvv 2572   ∖ cdif 2939  ∅c0 3249  {csn 3400  ωcom 4338  Ncnpi 6398

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 552  ax-in2 553  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036  ax-sep 3900  ax-iinf 4336

This theorem depends on definitions:  df-bi 114  df-tru 1260  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-ral 2326  df-v 2574  df-dif 2945  df-in 2949  df-ss 2956  df-int 3641  df-iom 4339  df-ni 6430

This theorem is referenced by:  enqex  6486  nqex  6489  enq0ex  6565  nq0ex  6566