Theorem nn0ex 9407

Description: The set of nonnegative integers exists. (Contributed by NM, 18-Jul-2004.)

Assertion

Ref	Expression
nn0ex	⊢ ℕ0 ∈ V

Proof of Theorem nn0ex

Step	Hyp	Ref	Expression
1		df-n0 9402	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 9148	. . 3 ⊢ ℕ ∈ V
3		c0ex 8172	. . . 4 ⊢ 0 ∈ V
4	3	snex 4275	. . 3 ⊢ {0} ∈ V
5	2, 4	unex 4538	. 2 ⊢ (ℕ ∪ {0}) ∈ V
6	1, 5	eqeltri 2304	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 2202  Vcvv 2802   ∪ cun 3198  {csn 3669  0cc0 8031  ℕcn 9142  ℕ₀cn0 9401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-cnex 8122  ax-resscn 8123  ax-1cn 8124  ax-1re 8125  ax-icn 8126  ax-addcl 8127  ax-addrcl 8128  ax-mulcl 8129  ax-i2m1 8136

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-uni 3894  df-int 3929  df-inn 9143  df-n0 9402

This theorem is referenced by:  nn0ennn  10694  nnenom  10695  uzennn  10697  xnn0nnen  10698  wrdexg  11123  expcnvap0  12062  expcnvre  12063  expcnv  12064  geolim  12071  mertenslem2  12096  eftlub  12250  bitsfval  12502  bitsf  12506  1arith  12939  znnen  13018  psrval  14679  fnpsr  14680  psrbag  14682  psrbasg  14687  psrelbas  14688  psrplusgg  14691  psraddcl  14693  psr0cl  14694  psr0lid  14695  psrnegcl  14696  psrlinv  14697  psrgrp  14698  psr1clfi  14701  mplsubgfilemm  14711  mplsubgfilemcl  14712  plyval  15455  elply2  15458  plyf  15460  elplyr  15463  plyaddlem1  15470  plyaddlem  15472  plymullem  15473  plyco  15482  plycj  15484  plyrecj  15486  clwwlknonmpo  16278