Theorem nn0ex 9502

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 9497	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 9243	. . 3 ⊢ ℕ ∈ V
3		c0ex 8268	. . . 4 ⊢ 0 ∈ V
4	3	snex 4298	. . 3 ⊢ {0} ∈ V
5	2, 4	unex 4562	. 2 ⊢ (ℕ ∪ {0}) ∈ V
6	1, 5	eqeltri 2305	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 2203  Vcvv 2813   ∪ cun 3209  {csn 3689  0cc0 8127  ℕcn 9237  ℕ₀cn0 9496

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-un 4554  ax-cnex 8218  ax-resscn 8219  ax-1cn 8220  ax-1re 8221  ax-icn 8222  ax-addcl 8223  ax-addrcl 8224  ax-mulcl 8225  ax-i2m1 8232

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-uni 3915  df-int 3950  df-inn 9238  df-n0 9497

This theorem is referenced by:  nn0ennn  10795  nnenom  10796  uzennn  10798  xnn0nnen  10799  wrdexg  11235  expcnvap0  12188  expcnvre  12189  expcnv  12190  geolim  12197  mertenslem2  12222  eftlub  12376  bitsfval  12628  bitsf  12632  1arith  13065  znnen  13149  psrval  14814  fnpsr  14815  psrbag  14817  psrbagaddclfi  14825  psrbasg  14829  psrelbas  14830  psrplusgg  14833  psraddcl  14835  psr0cl  14836  psr0lid  14837  psrnegcl  14838  psrlinv  14839  psrgrp  14840  psr1clfi  14843  mplsubgfilemm  14853  mplsubgfilemcl  14854  plyval  15597  elply2  15600  plyf  15602  elplyr  15605  plyaddlem1  15612  plyaddlem  15614  plymullem  15615  plyco  15624  plycj  15626  plyrecj  15628  clwwlknonmpo  16423  depindlem1  16501  depindlem2  16502